Context and motivation. The semantic review, a process that combines the manual inspection and formalisation of requirements with an automatic formal analysis, can help to improve requirements quality and find severe defects. Problem. The human needs tool support for inspection, formalisation and review of findings to be able to execute their part of the process efectively and ecfiiently. Solution. The new version of the Hanfor tool combines the existing formalisation editor with new features: reporting, lightweight checks, and the integration of formal analysis. Conclusion and results. We report on the addition of the new features to Hanfor and explain how they can help the human to execute their part in the semantic review process.
analysis tool (Subsection 3.4), and telemetry which allows us to measure how the human efort distributes over the single steps in the formalisation and inspection process (Subsection 3.5).
We call a requirements review a semantic review ibfyitreipnrtoedguractteiosnthoef tihnespreeqcutiiorenmoefnrtesqausiraefmoremntasl rreaqw. Hanfor report artefact and the (automatic) formal analysis of said formal artefacts in conjunction. More precpiascetlfyu, lindeafescetms(aen.gti.carmevbiiegwui,tyinospreilclteigoinbifloitryi)mis- Custoℬ mer Supervisor Worker Supervisor Custoℬ mer supported by deciding on a formalisation while Figure 1: Hanfor in the semantic review process. detection of defects in the complex behaviour of the requirements (e.g. inconsistencies) is solved by an automatic (exhaustive) analysis.
Here, we will include a short summary of the semantic review process that we apply (for a
comprehensive overview, see [
The work in Hanfor is mainly performed by the worker role, thus we will from here on mainly focus
on their interaction with Hanfor. In a Hanfor session, the worker is shown a table of requirements
(Fig. 2). By clicking on a requirement, the formalisation dialogue is opened; a formalisation can be
entered by selecting a scope (e.g. Globally) and a pattern (e.g. it is always the case that if ‘R’ holds then
‘S’ holds after at most ‘T’ time units) and filling the placeholders with according expressions (Fig. 3).
During formalisation, the worker sets tags (Sec. 3.1) for violations of requirements quality attributes and
other impediments to formalisation. For each tag, a detailed explanation can be added in the comment
ifeld (Fig. 4). The formalisation is accompanied by supporting tools, such as, variable autocompletion,
type-checking and -inference [
After a larger set of requirements has been formalised, the worker can decide to run fast internal checks (Sec. 3.3) and the exhaustive formal analysis in Ultimate ReqCheck1 (Sec. 3.4). The worker evaluates the results produced by the analysis and decides if the formalisation has to be adapted, if the ifnding is an artefact of the formalisation and has to be ignored, or if the finding is a true positive.
At this point, the worker has done their part and the supervisor reviews the findings. The final report is then presented to the customer. Both the formalisation process and the entire semantic review process may be iterated based on resolved findings on the supervisor and customer side, respectively.
The implementation of Hanfor is based on Python 3.12 and the web application framework flask on the server side, as well as JavaScript on the customer side. It relies on a number of third party tools, being either directly integrated (e.g. the SMT-solver Z3 via pysmt), connecting via remote API (e.g., the Ultimate-framework) or only suggested for combined usage (e.g. the version control system git).
The architecture (Fig. 5) of Hanfor is based on modules sharing a commonly accessible data storage and that supply their own web/API endpoint handling complex interactions (in a loose MVC fashion).
The session storage relates to the data of a single formalisation project, with revisions (snapshots of the project) that relate to each update of the requirements document by the customer. To be able to delegate any further version handling to git, the storage is based on JSON-files with versioning friendly (i.e. deterministic) updating. To enable rapid development, any module can register classes at the session storage, which are automatically saved and restored.
Functionality that is directly interacting with tags, variables, requirements and formalisations resides in the core-library to enable complex operations on this data. Parts of modules that are to be commonly 1Hanfor and Ultimate ReqCheck are available under https://github.com/ultimate-pa. used are also moved to the core library (e.g., Req to Pea started as part of the simulator but is now being used in some quick checks and thus was recently moved).
On the web-facing side, we make heavy use of flask-blueprints to separate the user-facing functionality (server side as well as customer side) from the core functions.
Regarding our previous publication on Hanfor [
A tag can have a general description to document the intention of this particular tag, and can be marked as process only in order to be excluded in any reports generated (as process tags are usually of no value for the customer). As soon as a tag has been defined by adding it to a requirement, it is listed on the Tags page, where it can also be edited. Hanfor also comes with a number of generally applicable standard tags for defects and communication.
During our case studies, tags turned out to be useful, but additional documentation and communication was required to convey the reasoning behind a large fraction of individual instances of tags. To allow this documentation to happen directly in Hanfor and also for it to be included in the report to the customer (except for comments on process tags), Hanfor shows a text field for each tag added (Fig. 4). This text field can be used to elaborate on the tag.
Recently, we started to use the tag-comment system to also show and store findings of tools such as the type checker and even the formal analysis (see Sec. 3.4). Experience in several industry projects
Ultimate Connector req xls t m s y p t m s y p e t a m i t l U
e h c a C itg j-tce b O n o s J
t m s y p
shows that the tags are useful for a quick overview and structuring of findings, while the comments have replaced any additional documentation outside of Hanfor as used in older semantic review projects. 3.2. Simulator Analysing the interaction of a small set of formal requirements or even of an edge case of a single formal requirement by hand is complex and time-consuming. The simulator ofers a graphical interface (Fig. 6) to simulate the behaviour of a selected set of requirements directly in Hanfor.
During simulation, the values of all relevant variables are shown in a timing diagram. To control the simulation, the user can enter concrete values that should be set in the next step and the duration of the next step. After clicking the Check-button, the simulator ofers a number of possible assignments for all free variables. The Next-button advances the simulation accordingly, while Back reverts the last selected interval (repeatedly).
In the bottom of the simulator, the formalised requirements are additionally shown as their logical
formulas (for details regarding the underlying logic, see [
Experience shows that the simulator is used sparingly, as inspecting the behaviour is relatively
time-consuming. In the occasion the simulator is used, it is an efective tool to inspect if combined
requirements behave the way intended in the formalisation, or if, e.g., an unwanted deadlock is
encountered when the formalisations are triggered. It is equally efective in refreshing one’s memory of
the exact semantics of a requirements pattern.
3.3. Quick Checks
Hanfor supports the worker by providing feedback on the quality of formalisations as early as possible.
While we perform exhaustive formal analyses in an external tool (see Sec. 3.4), all checks that can
possibly be performed in line with the formalisation are directly executed in Hanfor. This started
with simple checks like syntactical correctness and type checking/inference [
Requirements sets may define admissible values or value ranges for variables mentioned in the requirements. Intuitively, to be complete, each value admissible should also be at least element of one observable in the requirements. Or, in other words, the requirement should at least mention each of the admissible values at least once (possibly also as part of a range). We call a failure to do so domain incompleteness, which can hint at an incompleteness in the raw-requirements or at a formalisation error. To check for domain incompleteness, we compute the union of all values in all observables (for each variable ), and check if ⊇ with being the set of all admissible values. If this is not the case, a value missing in as well as both the sets and are displayed, to guide investigation of the finding.
For example, in a set of requirements, the permissible values of speed were set to 0 ≤ speed ≤ 100. The two requirements containing the speed variable contain the observables speed < 30 and speed > 30. The check for domain incompleteness reported the value 30 not being referred to anywhere, which seems to be an omission in one of the observables.
Equally, in any requirement, no observable for a variable , should have only elements outside the admissible range. We call this failure domain incompatibility, which has to be either a defect in the raw-requirements or in the formalisation. To check for domain incompatibility, we check for each observable of variable if the observable value is wholly outside the environment ∩ ̸= ∅. If this is the case, the observable as well as the permissible values are reported.
With the same variable as from the example above, a requirement contained the observable speed >
FULLSPEED with the constant FULLSPEED = 100 being defined elsewhere. A domain incompatibility
was reported by Hanfor because the aforementioned requirement ties to exclusively set speed outside
the permissible range. We were able to track this defect back to the worker using the wrong comparative
symbol2.
3.4. Ultimate Access
While the quick checks allow for immediate feedback, a semantic review in Hanfor takes long to detect
complex defects (e.g. redundancy, rt-inconsistency and vacuity [
Technically, the Ultimate connector connects to the web-API of an instance of Ultimate ReqCheck running on a dedicated (usually more powerful) machine. As visible in the main view of Hanfor (Fig. 2), there is an Analysis tab in which the analysis process can be started by selecting a configuration (setting the respective parameters within Ultimate ReqCheck) and the set of requirements to be analysed. The analyses usually take between some minutes to several hours. Running analyses tasks can be seen by switching to the Analysis page.
After analysis is finished, findings ( i.e. a defect was found) are directly integrated into Hanfor as tags. Each tag refers to the kind of analysis, with additional information being supplied in the form of a comment containing the tool output. 3.5. Telemetry Unfortunately, scientific investigations into the formalisation process itself are rare, as the formalisation step is usually only seen as a necessary step to perform formal analyses and not as a valuable review activity. With the telemetry feature of Hanfor, we intend to get a more nuanced view of the requirements formalisation process as executed by our workers, i.e., which requirements are finished in no-time versus which requirements take long or are finally disregarded for formalisation. The telemetry will also give insight into Hanfor itself, as it tracks what features are used during the formalisation.
On the technical side, Hanfor was enabled to run a socketIO connection in combination with its REST -API (see Fig. 5), that is used to transmit events generated by the user interface. Events are emitted by e.g. opening or closing a page and opening a formalisation dialogue. Data generated this way is written into a server side time series database.
We are currently in the process of collecting data of five diferent workers tasked with each formalising
a slightly altered version of the pseudo real-world requirements published by Houdek and Raschke [
Data will be analysed for the formalisation times and interaction timelines with Hanfor.
Originally, the requirements formalisation tool Hanfor was developed out of the necessity to formalise requirements as precondition to formal analysis. Emergence of our semantic review process during industrial case studies, however, showed that the formalisation step itself is of far greater importance as an individual component i.e. leading to a thorough inspection even with little to no domain knowledge.
In this paper, we gave an overview of new features we added to Hanfor to support the inspection by enabling fast documentation as well as the quality of resulting formalisations. Furthermore, we presented the move of Hanfor to support research on requirements formalisation.
The development of Hanfor continues as part of an industrial validation project.
Authors N. Hauf, E. Henkel, V. Langenfeld, and A. Podelski were supported by the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research, Germany) under reference no. 03VP11880 SystemValid.