| 13 SAL Translator |
| 13.2 Translatable RSL constructs |
|
| |||||
| 13.1 Introduction | ||||||
Rigorous Approach to Industrial Software Engineering (RAISE)[1] development method is carried out as a sequence of steps, starting from the specification of the system at a high level of abstraction and progressing by successively adding details towards a more concrete specification. To follow the RAISE development method, several tools are available such as code generators for several languages, test cases, and for model checking.
Model checking is a technique for verification of models, used for ensuring the correctness of hardware and software systems. Basically it consists of three steps: model specification, properties specification and verification (if model satisfies the specifications). The model is usually expressed as a transition system and properties are written as formal specifications, often using temporal logic formulas (CTL*, CTL or LTL).
Model checkers tool, such as SPIN, SMV and SAL, allow one to do the verification. For this first it is necessary to specify the model and the properties using the appropriate language (the language defined for each tool).
Regarding RAISE tools and in particular the tool for model checking (developed in 2006 by Juan Perna [13]), it allows one to translate RSL (RAISE specification language) to SAL (see [14]). Later, verification can be done using the SAL model checker.
Model checking is aligned with the RAISE development method, because it allows the verification of properties in early stages of the development process. Once verified, the RAISE development process warranties the preservation of the properties until the actual implementation of the system.
The tool takes an RSL file and generates three different SAL translations. The difference between this three versions V1, V2 and V3 is that V1 does the verification under the assumption of confidence condition (CC) satisfaction, and V2 and V3 do not.
You must remember that "Confidence conditions are conditions that should probably be true if the module is not to be inconsistent, but that cannot in general be determined as true or false by an automatic tool" [15]. For example, a definition of a partial function without a precondition generates the CC "false".
Under assumptions in V1, all partial functions are considered as total and type well-formedness is taken for granted. But, in general, it is difficult to grant this, so it is important to use the automatic verification power of model checking to first verify the satisfaction of CC.
In order to check CC, V2 and V3 are generated. V2 (called "CC" version) allows to check CC. On the other hand, V3 (called "simple CC" version) allows to check CC but gives less diagnostic information.
When the tool translates an RSL file, it generates a file for each version. Also it generate other files, like SAL_TYPES.sal, SAL_GLOBAL.sal, IT_AN.sal, NT_AN.sal and BT_AN.sal. The last three contain the definitions of Integer type, Natural type and Boolean type respectively. More details about this can be found in the last section of the present report.
The following section shows which are the basic RSL constructs translatable to SAL. Section 13.3 shows how to write RSL transition systems and LTL assertions in order to use model checking technique, preceded by general overview about model checking. The specifications written following 13.3 will need to use the translatable basic RSL constructs described in section 13.3. Section 13.4 talks about V2 and V3: how RSL constructs are translated and how transition systems and LTL assertions are translated. Finally section 13.5 describes how to use the tool.
| 13.1 Introduction | ||||||
|
| |||||