Adapting models to model checkers, a case study : Analysing AADL using Time or Colored Petri Nets∗ Xavier R ENAULT, Fabrice KORDON Universit´e Pierre & Marie Curie, Laboratoire d’Informatique de Paris 6/MoVe 4, place Jussieu, F-75252 Paris CEDEX 05 [email protected]
, [email protected]
Abstract The verification of High-Integrity Real-Time systems combines heterogeneous concerns: preserving timing constraints, ensuring behavioral invariants, or specific execution patterns. Furthermore, each concern requires specific verification techniques; and combining all these techniques require automation to preserve semantics and consistency. Model-based approaches focus on the definition of representation of a system, and its transformation to equivalent representation for further processing, including verification and are thus good candidates to support such automation. In this paper, we show there is a strong requirement to automatically map high-level models to abstractions that are dedicated to specific analysis techniques taking full advantage of tools. We discuss this requirement on a case study: validating some aspects of AADL models using both coloured and time Petri Nets.
The increasing development of distributed real-time embedded (DRE) systems requires the definition of dedicated process to cope with multiple levels of concerns such as: (i) resource dimensioning (processor, memory, time, bandwidth, etc.), (ii) behavior expectation (causality of events, correct processing of all events, safety, etc.), and (iii) cost reduction. Furthermore, current systems now usually require multiple expertise from domain-specific engineers, system integrators, quality and assurance teams. In this context, Model Driven Engineering (MDE) is a convenient approach to gather those concerns as a set of combined but yet heterogeneous models. Current application of MDE advocate for a clear separation of concerns ∗ This
work has been partially funded by the ANR Flex-eWare project.
J´erˆome H UGUES, Institut TELECOM, TELECOM ParisTech, LTCI 46, rue Barrault, F-75634 Paris CEDEX 13 [email protected]
that are expressed by means of a several of models (from high-level specifications down to implementation models). Although they aim at defining an “ideal process”, they seldom address an important issue: how to combine models and tools in order to ensure both consistency between specification levels and the mapping of specifications into refined ones more suitable for analysis. There is a need for “Verification Driven Engineering” (VDE): the careful choice of design patterns, combined to Validation and Verification tools (V&V). In , we note this usually requires engineers to fully understands both benefits and drawbacks of V&V tools. This is crucial to use them in the appropriate conditions and avoid pitfalls like non-applicability of theory (such as schedulability analysis), or combinatorial explosion. This paper shows how to take advantage of one notation, AADL to support VDE. AADL is a generic modeling framework for designing real-time embedded systems. Our goal is to automate, according to the system property to be verified, the choice of both an appropriate tool and the corresponding mapping to a specification it may process. Such an approach should increase the use of formal specifications in software and thus the quality of produced systems without increasing design time. In particular, this work focuses on the behavioral analysis of AADL by means of Petri Net models, as an application of VDE. It illustrates how to take advantage of Petri Nets and their extensions for several types of properties to be checked (deadlock detection, schedulability dimensioning). This allows a more efficient prototyping (or MDE) approach in the development of real-time systems. The next two sections present AADL and Petri Nets. Then, section 4 details how we map an AADL model containing time information into a Time Petri net and how we can verify some important scheduling properties. Section 5 illustrates our approach on a simple example.
AADL and V&V
AADL  is an architecture description language dedicated to the design of DRE systems standardized by the SAE. AADL is component-centric and allows to specify both software and hardware parts of a systems. It allows one to define consistent block interfaces, and to separate them from block implementation. An AADL model is made of components. Software components (data, thread, thread group, subprogram, process) are distinguished from execution platform components (memory, bus, processor, device) and hybrid components (system). The behavior of a system (e.g. how functional blocks interact) is fully defined in the standard by mean of “properties” (attributes with a dedicated semantics) to progressively refine the semantics of a system, e.g. dispatching invariants, communication patterns. Non-functional properties applied to each model element. Non-functional aspects of components can be described within an AADL model such as thread dispatching condition (periodic or sporadic), interface specifications and how components are interconnected. These have a deep impact on the system’s behavior. Functional aspects (algorithmic specifications) are attached separately as source code by means of AADL properties. An introduction to AADL can be found in . AADL provides two major benefits for building DRE systems. First, compared to other modeling languages, AADL defines low-level abstractions including hardware descriptions. These abstractions are more likely to help designing a full system, close to the final product. Second, hybrid system components help to refine the architecture as they can be detailed later in the design process, allowing for successive stages of modeling, from early requirements down to executable models. AADL tools support schedulability analysis , dependability modeling  and automatic code generation . Furthermore, numerous works explored the mapping of AADL semantics onto formal specifications for the verification of behavioral properties. This has been performed in multiple experiments from AADL to BIP , LOTOS  or TLA . However, these works contemplate only a case study, whereas we strive at defining a generic mapping, automated in our O CARINA toolset.
Petri Nets and extensions
Petri Nets [9, 14] are a family of formal notations to describe the behavior of distributed and concurrent systems. They offer several facets, we first present basic Petri nets and then two extensions for analyzing AADL models.
Petri nets Petri Nets are composed with places that represent resources and transition that define constraints between places. Places hold tokens that are consumed or produced by transition according to a firing rule. The firing rule is the following: if all precondition places of a transition hold a sufficient number of tokens, the transition is fired. Corresponding tokens are removed from input places and other tokens are produced in output places.
Figure 1. Petri net example Figure 1 shows a simple Petri net modeling cars in a parking. In the initial state of the system, there are 3 tokens (cars ready to enter the parking) in place ready and 2 in place parking lots (2 lots availables). Transition get in is enabled and may thus be fired (several transition may be enabled at the same time and the interleaving semantics is then used there to show all possible execution of the system). When it fires, it consume one token from input places (ready and parking lots) and produces one token in in parking. Then, ready contains only two tokens, parking lots 1 and in parking 1 token. From this new state, both get in and get out can be fired. Colored Petri Nets Colored Petri nets are Petri nets in which tokens carry out information. This requires the declaration of “color domains” (data types) to type places and the marking they contain. The firing rule then not only relies on the presence of tokens in input place; it may implies some constraints on the token values. parking_lots
ready Class Car is 1..3; Var c, p in Cars; get_in [c=p] in_parking get_out
Figure 2. Colored Petri net example Figure 2 shows a variation of the model of figure 1. There we consider that parking lots (variable p in the model) are associated to a given car (variable cin the model). Initial marking of place ready contains 3 cars with their individual id ( represents tokens 1 to 3 according to the color domain Car). There are two parking lots numbered 1 and 2. Then, according to the firing rule of colored Petri nets, only cars 1 and 2 can enter the parking because there is
no lot for cars 3. This behavior is expressed by guard [c=p] in transition get in. We chose symmetric nets1  (SN) for this work. SN is a class of Colored Petri nets that takes advantages of symmetries in distributed systems. Time Petri Nets Time Petri nets  (TPN) are Petri nets where a time interval [a, b], with 0 ≤ a ≤ b ≤ +∞ is associated with each transition. Thus, an implicit clock is associated with transitions : this clock is reset when the transition is newly enabled. A transition cannot be fired until the clock reaches a and must be fired before the clock reaches b. A consequence of this firing rule is that the system reaches a deadlock when time constraints are contradictory. parking_lots
in_parking get_in [0,0]
out get_out [1,5]
Figure 3. Time Petri net example Figure 3 shows a new variation of the model of figure 1. as soon as it is enabled, get in must fire immediately while we consider cars to be parked between 1 and 5 time units (the [0, +∞] interval is used to model Petri net transitions). Clock values may be discrete or dense (for continuous time). In this paper we only consider discrete time. Verification Capabilities P...