Property Language

From TASTE
Revision as of 08:58, 21 July 2022 by Idragomir (talk | contribs)
Jump to: navigation, search

An important requirement in designing the property modeling languages was to provide an intuitive specification means for engineers, that would not require advanced formal modeling skills or knowledge. Since engineers using TASTE have a good grasp of SDL and MSC, the obvious choice is to use variants of these languages, with a few simple extensions allowing them to express safety properties.

Observers

Observers are a variant of SDL processes with extensions allowing them to observe the state of any component (TASTE SDL function), including all its internal variables, as well as all signal exchanges that occur in the system. Some states of the observer can be classified as error or success, which allows for specifying the intended/unintended behaviours of the system, therefore allowing to capture safety properties.

Syntax

Figure below shows an example of observer. The system components’ state is observable through the st variable, of type System State. This ASN.1 type is automatically generated by TASTE and mirrors the hierarchical structure of the entire system, with fields corresponding to all components, including their states, message queues and internal variables. As can be seen in the figure, the observer can make decisions based on system internal values, such as st.Flaps Monitoring.counter or st.Flaps Monitoring.state. The signal exchanges are monitored through a particular type of transition trigger, that is inexistent in SDL and was added for this purpose.

ClipCapIt-220721-095059.PNG

It can observe the input/output of a signal, its source, destination and transported data values. The classification of some states are error or success is done with a declaration (upper left corner of figure shown above). In addition, some states may carry an ignore mark: it means that the user is not interested in what the system does once they are reached; they allow to optimize the verification by pruning parts of the state space.

Semantics

Observers are executed synchronously with the TASTE system: after each system step, the observers are allowed to react to the events that happened in this system step and to the new system state. The model-checker will search for the reachability of error /success states, and possibly generate an execution scenario when one is found.

Boolean Stop Condition

A quite usual class of system properties are invariants: Boolean conditions over the system state that have to be satisfied throughout the execution. In our framework, such conditions are expressed through an observer that has a specific structure with two states: a “monitoring” state in which the negation of the invariant is continuously tested, and an “error” state to which they switch when the invariant is violated (see figure below).

ClipCapIt-220721-095328.PNG

In our tool framework, these negated invariants are called Boolean stop conditions (BSC). The tool generates automatically the observer skeleton when a BSC is created, and the user needs only to fill the negated invariant in the transition trigger. Representing BSC as observers allows for some flexibility, as the user can later modify the structure of the observer if the property that he intends to specify proves to be more complex.


Property Message Sequence Charts

Message Sequence Charts are designed to capture a trace or a set of execution traces of a system in terms of the involved entities (functions, in TASTE) and what messages they exchange. It is a descriptive languages and can represent the traces at any abstraction level deemed suitable; as such, it does not formally specify whether the captured trace(s) are complete or incomplete (i.e., abstracting away some entities or message exchanges). It can be used to describe either intended or forbidden execution traces, but this characteristic is also not formally specified. In order to be able to use MSC as a property specification language, it needs (1) to be extended syntactically to specify characteristics such as those mentioned above, and (2) to have a clearly defined semantics for all allowed interpretations.

Syntax Extensions and Informal Meaning

ClipCapIt-220721-095351.PNG

We propose four Boolean attributes that determine the meaning attributed to an MSC:

  • intended /unintended : is the MSC representing a desirable trace of the system or a forbidden

one?

  • strict/non-strict: is the MSC representing all messages on a trace, or may some be missing?
  • verify (all)/search (one): are all traces of the system supposed to conform to the MSC, or is it used to designate one possible trace among others?
  • from start/not from start: is the represented trace supposed to begin at the start of system execution or not? Note that this is different from the strict attribute: one may specify a strict trace, but which needs not start at the beginning of system execution.

Syntactically, these attributes are specified using keywords in a formal comment starting with property type. For clarity, the search/verify and intended/unintended keywords are mandatory, while the other two Booleans are set according to the existence or not of the keywords from-start and non-strict. Figure displayed above shows a safety property that expresses the fact that a specific sequence of two messages is forbidden at any point in any system execution. The sequence is therefore specified as search unintended. Not-from-start and strict are implicit, by the absence of the corresponding negated keyword, as explained above. Note that not all 24 combinations of these attributes are valid. In fact, the valid combinations are subsumed by the following BNF rule: Property type ::= (search [from-start | nonstrict](intended | unintended))|(verify [from-start] intended) (where as usual, [ · ] designates an optional part, and | designates a choice).

Semantics through Mapping to Observers

ClipCapIt-220721-095538.PNG
ClipCapIt-220721-095621.PNG

Property MSCs are given a rigorous semantics by mapping them to observers. The mapping depends on the four Boolean attributes mentioned previously. Consider the MSC from figure displayed above. Regard- less of the attributes, the core semantics of this MSC is given by an observer skeleton accepting the sequence specified by the MSC, as per the figure shown above. To ease understanding, we chose to represent the observers in a simplified state-machine view, which allows to represent the hierarchical/paral- lel states in a unique view; hierarchical/parallel states are supported in SDL, and by extension in observers, but their representation is not suited for printing. As illustrated by this example, a property MSC with K instances will be translated to an observer with a composite state with K paral- lel lanes, each observing the sequence of events for the respective MSC instance. Each lane k sets a Boolean variable endk to True when its entire sequence has been observed, and when all lanes have finished, the observer proceeds to a final state end. In addition, for every signal output/input, a specific Boolean variable is set to True when the output is observed, and tested when an identical input is observed, to ensure that the input corre- sponds to output. This ensures for example that, if the sequence shown in the figure above appears in a system execution preceded by another aa sig- nal, the two lanes start advancing over the same aa signal. The intended/unintended status of the MSC is reflected in the classification of the end state. The end state is marked with error if the MSC is labelled unintended, and success if it is labelled intended. With this basic structure in mind, we can examine the mapping for different MSC property types.

ClipCapIt-220721-104925.PNG

Figure displayed above shows the mapping of search non-strict MSCs. Note the transition that loops back on the main state: it allows the observer to non-deterministically restart the observation. This deals with the absence of the from-start attribute: it means that the sequence specified by the MSC may be observed at any point in the sys- tem execution, even if a prefix has already been observed. The non-strict character of the MSC is the implemented by the default semantics of observers, which ignore events that are not specif- ically matched by a transition trigger. Here, if for example a signal cc appears between aa and bb, it would be ignored by the observer.

ClipCapIt-220721-105016.PNG

For a strict MSC, on the contrary, some- thing needs to be added so that the observer can detect deviations from the sequence. Figure displayed above shows the mapping of a search from-start MSC (which is also, implicitly, strict). Note the tran- sition on the left, which takes the observer to state stop whenever a non-specified event happens. The figure is just an explanatory device – in real- ity, the generated observer will contain transitions for detecting deviations in all inner states of the main state, such that these are rendered “input- complete” with respect to any possible observable event of the corresponding instance. The state stop is marked as ignore to optimize exploration: indeed, the occurrence of an unexpected event is not an error for a search from-start MSC, it just means that the search has not yet found the right sequence. A verify from-start intended MSC will be mapped to the same observer as a search from-start, but with end state marked success and stop state marked this time as error.

ClipCapIt-220721-105112.PNG

Figure depicted above represents the semantics of a search MSC, where both the non-strict and from-start labels are absent. Then any I/O that concerns the represented instances and that does not appear in the MSC will lead to the ignore state stop, except from the initial/final state of each lane. In addition, the non-deterministic self- loop on the main state allows the observer to restart observing the I/O sequence from any point in the system execution. This is a powerful use of non-determinism in observers: a state in which the system has just performed an unexpected event, will have two successors, one that stops the explo ration (stop) and one that restarts the observer. Of course, this comes at a price: there is a potential combinatorial explosion of the state space size, as usual when one determinizes a non-deterministic automaton. It is no surprise that the search of a non-strict sequence of events is costly in terms of complexity. Finally, for a verify intended MSC, the semantics is given by an observer, but lacking the “restart” transition on the main state (self-loop on the left), and with end state marked success and stop state marked error. The absence of from-start is encoded in the fact that any other I/O not specified on the MSC is ignored in the initial state of each lane. The tool will generate the equivalent observer for a given MSC, depending on the specified attributes. The observer is in the same, readable format as any observer, and the user may check and possibly modify it to fit the specification needs. Since the semantics of the different variant is quite subtle, the users are in fact encouraged to do so, in order to check that what they specified in the MSC corresponds to their actual intention.