The demand for more and more complex Cyber-Physical Systems (CPS), i.e. tightly coupled hardware and software components that operate in a physical (unsupervised) environment, is increasing. More often than not, they require guarantees in terms of performance, safety, security, sustainability, etc. The design of CPS is therefore a fundamental, yet dificult and challenging task. The Cross-layer modElbased fRamework for multi-oBjective dEsign of Reconfigurable systems in unceRtain hybRid envirOnments (CERBERO) EU project [9] aims at developing a set of tools, cooperating at diferent layers of abstraction, to ease the design process and increase adaptivity of such systems. In this context, our research focuses on the analysis of the first item produced in the design process: software and system requirements. It is well known that a flaw in the requirements specification can lead to delays, additional costs and, possibly, the failure of the project. Nonetheless, due to the intrinsic dificulty of dealing with natural language sentences, requirements are often checked manually, an error-prone and time-consuming activity. Our goal is to design a tool to automatize this task and, starting from the formalization of requirements, generate artifacts that can be used to validate and verify the items produced along the design process.
1 Introduction
The definition and elicitation of requirements is usually the first step in the
design of software and cyber-pysical systems. They are used as a guideline for
the implementation and as a reference for the verification and validation of the
ifnal product (see, for example, the V-Model depicted in Figure 1 on the left,
often used in the design of CPS). Despite their importance, the assessment of
requirements is still largely carried out manually. The Requirements
Engineering (RE)[
This objective matches well with one of the main CERBERO’s missions, namely reducing the time-to-market of new designed CPSs by means of an integrated toolchain for comprehensive model-based design of CPS (Figure 1 on the right).
The first main challenge of our research is to evaluate requirements consistency: informally, it means detecting errors, missing information and deficiencies that can compromise the interpretation and implementation of the intended system behavior. At a syntactic level, this may involve the check for compliance with standards and guidelines, such as the use of a restricted grammar and vocabulary. We call this task Compliance Checking.
However, most of the inconsistencies reside at a semantic level, i.e. in their
intended meaning. Therefore, it is necessary to interpret the requirements
semantics and represent them with a formalism that allows for reasoning. How to
formalize and translate requirements into a formal representation is an open
research question. A recurrent solution in the literature is the use of Property
Specification Patterns (PSPs), first introduced by [
Given the set of requirements represented in a formal logic, it becomes
possible to implement more sophisticated checks and exhaustive reasoning. We
formally define this task Consistency Checking analysis [
Moreover, the formalization of requirements and the consistency checking are
enablers for other tasks we would like to tackle, namely the automatic
generation of test suites [
Knowledge Base Requirements
Feedback
Report Test Suite Monitor
Compliance
Checker
NL2FL Consistency
Checker
Automatic Test Generator
Runtime Monitor Builder
Formal Representation is useful to ensure that no unexpected behavior, which may have escaped the test phase, is executed at runtime on the target CPS. The full overview of the framework we intend to realize is depicted in Figure 2.
Finally, the choice of which logic to use largely afects the reasoning power and
the kind of requirements that can be formalized: qualitative, real-time and/or
probabilistic. For example, in some logics it is only possible to specify that an
event e will eventually happen in the future, while others can also constraint the
time frame (e.g. e will happen within 5s) or its likelihood (e.g. e will happen
with probability p 0:5). We started from Linear Temporal Logic (LTL)[
Consistency of Property Specification Patterns
Our first contribution [
Globally, it is always the case that if proximity_sensor < 20 holds, then arm_idle eventually holds.
We first translate every requirement ri 2 R in LTL(DC ), an extension of LTL over a constraint system DC = (R,<,=), with atomic constraints of the form x < c and x = c (where c 2 R is a constant real number and ‘<” and “=” have the usual interpretation). We then show how the new problem can be reduced to LTL satisfiability. Let X(ϕ) be the set of numerical variables and C(ϕ) be the set of constants that occur in ϕ. We compute: – the LTL(DC ) formula ϕi for every requirement ri 2 R; – the conjunctive formula ϕ = ϕ1 ^ ::: ^ ϕn; – a set Mx(ϕ) of boolean propositions representing possible values of x 2 X(ϕ); – the formula QM encoding the constraints over Mx(ϕ) 8x 2 X(ϕ); – the formula ϕ′ that substitute all x 2 X(ϕ) in ϕ with a set of boolean propositions from Mx(ϕ);
Given the LTL(DC ) formula ϕ over the set of Boolean atoms P rop and the terms C(ϕ) [ X(ϕ) we have that ϕ is satisfiable if and only if the LTL formula ϕM ^ ϕ′ is satisfiable. This result is important because it shows that LTL( DC ) is decidable and that we can exploit state-of-the-art LTL model checkers.
However, LTL satisfiability is not suficient to guarantee the correctness and
completeness of the requirements set, and a more extensive feedback is necessary
in case of inconsistency. In order to answer these needs, we extended the work
in [
Connected Requirements Check Given a set of requirements R = r1; : : : ; rn, we want to check if one or more of such requirements are completely unrelated to the others, meaning that they describe some behaviors that do not interact with the main bulk of the system. This may happen in an underspecified requirements set or for some spelling errors. To find these faults, we first build the undirected graph G = (V; E) representing the connections in R, such that: – vi 2 V 8ri 2 R; – (i; j) 2 E if X(ri) \ X(rj ) ̸= ∅ 8ri; rj 2 R; i ̸= j where X(ri) is the set of variables, boolean or numerical, that appear in ri. We then perform a static analysis on the graph, checking if: – a variable is never used to connect two requirements; – the graph is composed of two or more connected components. Both cases suggest that the system is underspecified, and a corresponding warning message is generated.
Consider, for instance, the set of requirements: R1 It is always the case that x >= 0 and x <= 10 holds.
R2 After x > 5, y or z eventually holds.
R3 It is always the case that if w > 10 holds, then y and z previously held. R4 Globally, it is always the case that if j holds, then k eventually holds. R5 Globally, it is always the case that if k holds, then j eventually holds. The corresponding graph is showed in Figure 3. In this case two warnings are generated: (1) The variable w is used only in R3; and (2) requirements R4 and R5 are part of a separated component, meaning that they are describing the behavior of a subsystem that does not interact with the main system, or some requirement is missing.
In the current implementation boolean and numerical variables are handled
in the same way, but a more fine grained check could take into account every
single range (in the example before, what happen when x is between 0 and 5?).
In case of inconsistent requirements, we are interested in finding a small subset
of them that explain the problem. This can help the designer in identifying
and fixing mistakes in a (possibly very large) set of requirements. We perform
this task, called Inconsistent Requirements Explanation, using the deletion-based
algorithm represented in Algorithm 1. The algorithm finds an high-level minimal
unsatisfiable core (HLMUC) [
To better illustrate how the algorithm works, consider the following example: R1 Globally, it is always the case that A holds.
R2 Globally, it is never the case that A holds.
R3 Globally, it is always the case that B holds.
R4 Globally, it is always the case that if B holds, then C holds as well. R5 Globally, it is never the case that C holds.
R6 Globally, it is always the case that A and B holds.
R7 After B, D eventually holds.
In this case it is simple to see that there are 4 HLMUC in R: fR1; R2g, fR2; R6g, fR3; R4; R5g, fR4; R5; R6g. Algorithm 1 finds only one of these sets, depending on the evaluation order. A possible step-by-step execution is illustrated in the following table.
The final result is R′ = fR4; R5; R6g, but if we used the inverse order, we would have obtained R′ = fR1; R2g.
Algorithm 1 is pretty simple although ineficient, because it performs jRj
satisfiability checks. We also implemented a faster algorithm that employs a
recursive strategy, but it has been omitted due to space constraints.
Algorithm 1 Linear Deletion-Based Inconsistency Finder Algorithm
We are now working on the problem of automatic tests generation from LTL
specifications. This is a widely studied problem [
Moreover, the consistency checking of requirements has been improved in the
current paper, but more work is necessary in order to validate the specification.
We plan to add more checks in parallel with the current ones, like the
Realizability Check implemented in [
Finally, for future works we would also like to both extend the natural
language interface with less restrictive constraints and explore more expressive
formalisms. In this regard, two research directions are possible: extend the current
work with probabilistic or real-time logics, or introduce the contract-based design
paradigm. This paradigm is an emerging solution to deal with complex systems
by decomposing them in components and defining their properties in term of
contracts [