The analysis of legacy systems such as electro-mechanical circuits requires the extraction of the underlying specification from a high level point of view. We consider P-stable abstraction, an analysis for transition systems that synthesizes the properties of a given set of events in terms of their eventual and stable efects on the system state. The abstract transitions simulate convergent runs of the concrete model and correspond to a set of temporal properties which are satisfied. We show an application of the P-stable abstraction on a relay-based circuit, showing its ability to extract a high level description of the implemented behaviour.
level of abstraction needed to specify the software control. Our aim is to automatically build a high level description of what are the behaviours exposed by a circuit in response to external events. The specifications extracted from the transition system of the analogue circuit will be cross checked on the new software-based implementation model. Since the two systems we want to compare rely on diferent sets of variables, we want to synthesize properties defined on the common ones, i.e., the high level observable railway properties, such as the status of a semaphore lamp or a railroad switch. In addition to this “static” abstraction of a state by quantification of the local variables, we consider more sophisticated path-based abstractions. Two implementations may realize a certain behaviour in a diferent number of internal steps or by passing through diferent intermediate conditions. For this reason, in order to extract the high level efects of an event, we shall consider its eventual stable target. 2. P-stable Abstraction P-stable abstraction has been firstly introduced in [ 7] for the characterization of the stabilization behaviour of a hybrid system. This concept is built on two main elements: (a) the set of properties of interest P, defining the granularity of the abstraction; (b) the set of external events acting on the system, whose specifications we want to extract.
Stability is defined in terms of the set of predicates P. Intuitively, given a P-representable region , i.e., a region expressible as a boolean combination of predicates in P, a state is stable in if it can exit from it only by means of an external event. In other words, if the system is untouched, all the evolutions of remain in ( |= AG) 1. When assessing stability, the minimality of the region is also required: namely, must be the most precise representation available in the grid induced by P on the state space.
Stability can be broken by an external stimulus ∈ which triggers an evolution that will converge in a possibly diferent region ′ (i.e., →− ′ and ′ |= EFAG′). In the context of hybrid systems, this run-to-completion process can involve both discrete and continuous internal transitions.
The P-stable abstraction of a transition system is a finite state automaton whose locations are P-stable states. With respect to the known predicate abstraction [8], here, an abstract transition simulates a convergent path in the closed system and the length of the run is not preserved. Moreover, the predicates are not evaluated in transient states, i.e., before stability is obtained.
The P-stable abstraction simulates all the runs of the underlying system, provided that the external stimuli do not occur too frequently: it disregards runs in which an event interrupts a stabilization still in progress. This restriction is justified when considering human controlled devices that have a fast internal response.
By taking into account the duration of this stabilization process, the abstract automaton can be enriched with timing information. The timed P-stable abstraction automaton is a timed automaton whose transitions are equipped with an interval which must be inclusive of all possible convergence times. The timing extension of the P-stable abstraction is able to provide the maximum frequency at which the system is allowed to receive inputs, i.e., the value of a slow-switching constraint for the external environment that makes the abstraction sound. 1‘|=’ is a shortcut meaning that the model transition relation is restricted to internal events. close
Lever 000 000
100 close δ = 2 C 100
110 close J
δ = 1 111
011 close C close
Lever
000 111 111 cloRse 111Loepveenr011 opCen 011
Loepveenr [0, 0] 011
Computation via abstract interpretation. [7] formulates the problem in the general framework of abstract interpretation [9] which provides a formal setting to trade precision for eficiency. P-stability is defined in terms of a Galois connection (using sets of states as concrete domain and sets of formulae as abstract domain). Sound overapproximations are then obtained by composition with further connections on simpler domains: in particular the abstraction can be made deterministic, by joining the possible next stable formulae, and stable regions can be overapproximated with their cartesian abstraction (therefore losing relational combinations between predicates in P).
The algorithm for the deterministic cartesian abstraction has been implemented with an abstract reachability analysis, manipulating LRA formulae by combining BDDs (with the CUDD library [10]) and convex polyhedra (with the PPLite library [11]).
Consider the circuit shown in the left-hand side of Figure 1. The involved components are a voltage generator, three relays and four switches. A relay is an electro-mechanical component able to control a remote switch: when the current that flows in it is above a certain threshold, we say that the relay is activated and its magnetic field can close (or open) a remote switch. A relay may require some time in order to activate after the current starts flowing: we consider relays C and J with an activation delay of 1 and 2 seconds respectively, and a relay R, whose activation is instantaneous. The deactivation process is immediate for all of them. All the switches are controlled by a “master”: switches C, J, R are closed if and only if the homonym relay is active; switch Lever, instead, is controlled by an external operator.
The circuit is modeled with a hybrid automaton ℋ with 77 continuous variables and 18 boolean variables. At the top of the right-hand side of Figure 1 we show a concrete run of ℋ; below it, we show the (deterministic and cartesian approximation of the) corresponding P-stable abstraction obtained with predicates P = {activeC, activeJ, activeR}, and events = {closeLever, openLever}. For exposition purposes we label a state with a vector ∈ {0, 1}3 whose positions denotes the active status of relays C, J, R respectively.
Initially, all the relays are inactive and all the switches are open: the system is stable in state 000. When Lever is closed, current starts to flow in relay C and after = 1 it gets activated. With a discrete transition, it closes the corresponding switch, allowing relay J to start its activation process. After = 2, another discrete transition closes switch J and relay R is immediately active. It follows that the closure of Lever triggers a run-to-completion process towards state 111, whose convergence time is 3 seconds. Starting from this state, if Lever opens, then relay C gets deactivated: nonetheless, thanks to the switch R, relay J continues to receive current and the system is stable in state 011. If Lever closes again, the system only requires the activation of relay C to converge again in state 111 after 1 second.
We have synthesized the P-stable abstraction which highlights the stable states, i.e., the ones from which the system can exit only with an external event. Each transition is equipped with a time interval, defining the duration of the convergence process: in this case, it defines that if two subsequent inputs are separated by at least 3 seconds, then the system has always suficient time to stabilize and the P-stable abstraction is a sound simulation of all its behaviours.
The reverse engineering value of the obtained automaton relies on the abstraction of the transient states, which are proper of this particular implementation of the desired logic. As an example, a state in which R is active but the corresponding switch is still closed is disregarded, since this process is actually instantaneous and introduced only by the modeling choices. As a matter of fact, instantaneous transitions between the activation of a relay and the action on the corresponding switch are fundamental to faithfully model the causality of the events, especially with circular topologies, but have no physical relevance. Moreover, also the states which are reachable only within a process with a non-null convergence time are skipped: consider that “activeR ↔ activeJ” is not an invariant of the circuit, but it is respected in the P-stable abstract automaton.
We presented P-stable abstractions, an approach proposed in [7] for the extraction of the properties that a hybrid system satisfies. We showed its application on a relay circuit.
In the future we are considering a more general stability-abstraction framework, able to
provide diferent levels of expressiveness and precision for reverse engineering purposes.
[4] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri,
S. Tonetta, The nuXmv symbolic model checker, in: CAV, volume 8559 of Lecture Notes in
Computer Science, Springer, 2014, pp. 334–342.
[5] A. Cimatti, A. Griggio, E. Magnago, M. Roveri, S. Tonetta, Extending nuXmv with timed
transition systems and timed temporal properties, in: CAV (