Article Preview
TopIntroduction
Verifying complex and real-time systems is a major challenge, especially in the industrial field. In this context, it is important to ensure behavioral compliance between the developed system and the requirements. In the past few decades, various formal methods (ex: model checking (Moon, Powers, Burch, & Clarke, 1992)) and property languages have been proposed as a rigorous and robust solution to help designers create flawless systems. Model-checking is a formal approach to software behavioral compliance checking. In this approach, the requirements are specified as properties in formalisms such as Linear temporal logic (LTL) (Pnueli, 1977) (Halbwachs N. a., 1994) or Computation Tree Logic (CTL) (Emerson & Sistla, 1984). Although these techniques and languages are notably expressive and allow for rigorous expressions, many of them involve formalisms that might be extremely intricate to be broadly adopted by industry engineers in their verification activities.
Another method, for the expression of requirements popularized by the LUSTRE language, is based on the notion of observer (Halbwachs N. a., 1994; Halbwachs, Lagnier, & Raymond, 1994). The testing process based on a parallel composition of the observer and the tested system consists of performing reachability analysis in the composed system. The expression of properties to be checked is more manageable in the form of an observer. However, writing such an automaton can nevertheless prove to be complex when the property itself is complex. Many authors have reported this finding, and some of them (Konrad & Cheng, 2005; Smith, Avrunin, Clarke, & Osterweil, 2002) have suggested formulating properties using the concept of “Definition Patterns” originally introduced by (Dwyer, Avrunin, & Corbett, 1999). They proposed a property specification language based on the composition of predefined patterns and scopes. A pattern expresses a temporal property on execution, seen as sequences of state/event. Each pattern can be associated with a scope that defines the parts of executions on which the pattern must hold. Yet, many authors revealed how painful it is for non-experts to express properties using (Dwyer, Avrunin, & Corbett, 1998) definition patterns. To handle this problem, Dhaussy et al. (Dhaussy, Auvray, De Belloy, Boniol, & Landel, 2008) define a specification language named CDL that gathers the main concepts proposed by (Konrad & Cheng, 2005; Smith, Avrunin, Clarke, & Osterweil, 2002; Dwyer, Avrunin, & Corbett, 1999) and allows the expression of properties (safety, invariance or liveness) more easily. Moreover, they implement an Observer-Based Prover (OBP) tooling that transforms properties into non-intrusive observer automata with reject states. The property verification process consists of a reachability analysis on the exploration graph rising from the composition of the tested model and the observer. If one of the reject states is reached, that means that the checked property is not valid.
This work shows that the CDL language can be easily extended to express further properties (1) by adding new variants of patterns (scopes and options). It proposes to adopt an observer automata-based semantics (2) that is well-suited to verify properties using OBP or other model-checking tools.
This paper is structured as follows. Section 2, provides a short introduction to the original property specification patterns system proposed by Dwyer et al. and evokes the specification language CDL suggested by (Dhaussy, Auvray, De Belloy, Boniol, & Landel, 2008). Section 3 provides an overview of the observers' automata. Section 4 presents the proposed extended CDL patterns, scopes and options. Section 5 shows the expressiveness of the extended CDL patterns compared to the original one. Section 6 highlights remarkable related works. Finally, Section 7 concludes and supplies a perspective of future works.