QUACK Technology Platform

A Platform for the Quality of New

Generation Integrated Embedded Systems

Author: Andrea Baldini, Giovanni Denaro, Marco Di Natale, Alessandro Fantechi, Andrea Fedeli, Angelo Morzenti, Mauro Pezzè, Paolo Prinetto, Davide Rogai, Emilio Spinicci

Date: December 2002

Doc. Id.: D1.1

Quack Research Units

Unit 1: Università degli Studi S. Anna di Pisa UniPi

Unit 2: Università degli Studi di Firenze UniFi

Unit 3: Politecnico di Milano PoliMi

Unit 4: Università degli Studi di Milano – Bicocca UniMiB

Unit 5: Politecnico di Torino PoliTo

Scientific Coordinator: Mauro Pezzè UniMiB

Type: Technical

Status: Final version

Availability: Deliverable

Document History

V1.0 Initial version for comments

V1.1 Added contributions. TRIO and complementary aspects of TRIO and TILCO (by Angelo Morzenti, PoliMi); model checking for fault-tolerance (by Emilio Spinicci, UniFi); timing analysis on SDL models (by Andrea Fedeli, UniFi); generation of functional test cases (by Andrea Baldini, PoliTo);

V1.2 Added contributions from UniFi and UniPi. Some contribution from UniFi is still missing.

V1.3 Final version

Abstract

This document aims at defining a methodological and conceptual platform common to all the Research Units cooperating in the QUACK project. The document presents an analysis of models and technologies proposed by the QUACK Research Units for the project, a comparison of the different models and technologies, a detailed analysis of compatibility and consistency of the different models, and the definition of a conceptual platform for the logical and physical integration of models, technologies methods and tools, aiming at both identifying synergies and eliminating possible inconsistencies among them.

Contents

1. Introduction 4

2. Background Technology 5

2.1 Formal specifications of Real-time embedded systems 5

2.1.1 TRIO 5

2.1.2 TILCO 12

2.1.3 Complementary aspects of TRIO and TILCO 19

2.2 Model checking for analyzing fault-tolerant systems 20

2.3 Schedulability analysis 22

2.3.1 Schedulability Analysis Algorithms 23

2.3.2 Timing analysis on SDL models 27

2.3.3 Timing analysis on UML Models 28

2.3.4 Patterns for schedulability analysis in UML 2.0 (UML and SDL merger) 29

2.4 Generation of functional test cases 30

2.4.1 Assumptions 30

2.4.2 Process definition 31

2.4.3 Test generation 31

2.4.4 Translation process 33

2.4.5 Test Preparation 34

2.4.6 Test Translation: Mapping phase 34

2.4.7 Test Translation: Pre-sequencing Phase 35

2.4.8 Test Translation: Sequencing phase 35

2.5 Generation of test cases for concurrent and object oriented systems 36

2.5.1 Intra- and inter-class testing 36

2.5.2 Testing polymorphism and dynamic binding 38

2.5.3 Mutation analysis of concurrent systems 40

3. A Common Conceptual Platform 41

4. Conclusions 43

References 43

1. Introduction

The main objective of the QUACK project is to define a new integrated methodology to control the quality of heterogeneous, modular and configurable embedded systems. To this end, it is important to preliminarily understand the impact of state-of-the-art technologies on the different phases of the development process for these systems, especially for the difficult tasks of initially defining the system, designing and assessing the system components, and designing and assessing the component integration.

Different state-of-the-art technologies are available in the Research Units that cooperate in the project. These include:

- Temporal logics that can be used for modeling and analyzing user requirements, and in particular:

- Logic specification of RT software systems by means of TRIO (a temporal logic with metric on time), methodologies for property-proving based on both model checking and theorem proving, and techniques for generating test cases from logic specifications[CC99, GM01, MMM95]

- Logic specification and automatic code derivation using the Temporal Interval Logic with Compositional Operators (TILCO)[MN01];

- Techniques for analyzing fault tolerant systems and validating non-functional requirements[FGS99, GLM99, BFS00];

- Techniques and algorithms for establishing the correct scheduling of time-critical systems and for analyzing timing properties (e.g., the feasibility of critical deadlines) of compound systems, based on both UML and SDL models[But97, ABDS98];

- Techniques for testing object oriented and component based systems, and in particular:

- Techniques for test case generation from UML diagrams and test coverage metrics based on UML diagrams[BBP01];

- Techniques for automatic execution of test cases for embedded systems[BBM02]Techniques for testing the state of classes of object oriented software[BOP00];

- Techniques for testing the state of classes of object oriented software[BOP00];

- Techniques for testing object oriented software in presence of polymorphism[OP99];

- Techniques for testing concurrent software systems[FP02].

This document aims at defining a methodological and conceptual platform common to all the Research Units cooperating in the QUACK project. In fact, it is important to establish the logical and physical integration of the various notations and technologies that are available in each Research Unit, and which might be employed in the project, aiming at identifying beneficial synergies and eliminating possible inconsistencies among them.

The definition of a common methodological and conceptual platform is based on the evaluation of the mutual compatibilities of proposed notations and techniques. More specifically, this document presents and compares the various descriptive and operational models that the Research Units use for modeling the initial requirements, the architecture of the systems, the constraints and invariants of both each component in isolation and the system as a whole, the behavioral assumptions, and the scheduling. We also discuss and compare the testing and analysis techniques, which can be applied in the project.

This document is organized as follows. Section 2 presents the technologies that each Research Unit uses and which are applicable in the project. Section 3 compares the proposed technologies, aiming at identifying synergies and inconsistencies, and sketches the methodological and conceptual platform for the project. Finally, Section 4 summarizes and concludes the document.

2. Background Technology

This section presents the technologies that the QUACK Research Units contribute to the project.

2.1 Formal specifications of Real-time embedded systems

2.1.1 TRIO

TRIO is a first order logical language, augmented with temporal operators which permit to talk about the truth and falsity of propositions at time instants different from the current one, which is left implicit in the formula.

Like in most first order languages, the alphabet of TRIO is composed of variable, function, and predicate names, plus the usual primitive propositional connectors ‘¬’ and ‘®’, the derived ones ‘Ù’, ‘Ú’, ‘«’, ..., and the quantifiers ‘$’ and ‘"’.

Variables, functions, and predicates are divided into time dependent and time independent ones. This allows for representing change in time. Time dependent variables represent physical quantities or configurations that are subject to change in time, and time independent ones represent values unrelated with time. Time dependent functions and predicates denote relations, properties, or events that may or may not hold at a given time instant, while time independent functions and predicates represent facts and properties which can be assumed not to change with time.

Unlike classic first-order theories, TRIO is a typed language: a domain of legal values is associated with each variable, a domain/range pair is associated with every function, and a domain is associated with all arguments of every predicate. Among variable domains there is a distinguished one, called the Temporal Domain, which is numerical in nature: it can be the set of integer, rational, or real numbers. Functions representing the usual arithmetic operations, like '+', '-', '*', '/', and time independent predicates for the common numerical relations, like '=', '¹', '<', '£', are predefined at least for values in the temporal domain.

TRIO formulas are constructed in the classical inductive way. A term is defined as a variable, or a function applied to a suitable number of terms of the correct type; an atomic formula is a predicate applied to terms of the proper type. Besides the usual propositional operators and the quantifiers, one may compose TRIO formulas by using primitive and derived temporal operators.

There is one primitive temporal operator, Dist, that allows the specifier to refer to events occurring in the future or in the past with respect to the current, implicit time instant. If F is a TRIO formula and t is a term of the temporal type, then Dist(F, t) is a TRIO formula that is satisfied at the current time instant if and only if F holds at the distance of t time units from the current one: in the future if t>0, in the past if t<0, or at the current time if t=0. Based on the primitive temporal operator Dist, numerous derived ones can be defined. A sample thereof is given in the following able.

Operator / Logical Definition / Intuitiva meaning
Futr(F, d) / d³0 Ù Dist(F, d) / Future
Past(F, d) / d³0 Ù Dist(F, -d) / Past
Lasts(F, d) / "d'(0<d'<d ® Dist(F, d')) / F holds over a period of length d in the future
Lasted(F, d) / "d'(0<d'<d ® Dist(F, -d')) / F held over a period of length d in the past
Alw(F) / "d Dist(F, d) / F always holds
SomF (A) / $d(d>0 Ù Dist(F, d)) / Sometimes in the future F will hold
Within(F, d) / $d'(0<d'<d Ù Dist(F, d')) / F will occur within d time units
UpToNow (F) / $d ( d > 0 Ù Past (F, d) Ù Lasted (F, d) ) / F held for a nonnull time interval that ended at the current instant
Becomes (F) / F Ù UpToNow (¬F) / F holds at the current instant but it did not hold for a nonnull interval that preceded the current instant
NextTime (F, t) / Futr (F, t) Ù Lasts (¬F, t) / the first time in the future when F will hold is t time units apart from the current instant

Notice that the operators of classic temporal logic can be easily obtained as TRIO derived operators. For instance, SomF corresponds to the “Eventually” operator of temporal logic. Also, it can be easily shown that the operators of several versions of temporal logic (e.g., interval logic) can be defined as TRIO derived operators. This shows that TRIO properly extends temporal logic and argues in favor of its generality since many different logic formalisms can be described as particular cases of TRIO.

Another useful short-notation provided by TRIO is the application of the Dist, Futr, and Pat operators to a term rather than to a formula: for instance, Past(s,t) denotes the value of term s at the instant laying t time units in the past from the current one.

Example

As an example of a TRIO specification consider a small fragment of the specification of a digital energy and power meter. The meter is composed of a magnetic transducer that converts the energy flow through the line into the rotation of a disc. In the peripheral part of the disc transparent and opaque portions are evenly alternated, with the purpose of permitting the detection of the disc motion and its velocity (which are respectively proportional to energy and power consumption) by means of a photocell. To minimize its wear, the photocell is activated only for a small fraction of the total working time of the meter. Its activation is performed according to the diagram shown in Figure 2.1.1.

Figure 2.1.1. Timing diagram for the photocell activation.

Once the photocell is activated, the acquisition of its signal must be postponed by a delay d, to permit it to reach a stable state. The cell activation lasts only d1 time units, and it is repeated after d2 time units.

We formalize this description in the following way: first, we define two time dependent 0-ary predicates, activation and acquisition, with obvious meaning. Then, the next two formulas specify the timing constraints on the activation and acquisition predicates, respectively.

At the instant of acquisition the photocell may be in one of two states which correspond to the detection of a transparent or opaque portion of the disc. We thus model the photocell state by a time dependent variable position ranging in the set {open, closed}.

The consumption of an energy quantum is detected when the disc moves from a transparent portion to an opaque one, or vice versa, and in the following formula it is modeled by the time dependent 0-ary predicate quantum, which may be true only at times when the acquisition takes place, if the current photocell state is different from the preceding one.

2.1.1.1 TRIO’s formal semantics and executability

As mentioned above, a major feature of the TRIO language is its executability. This allows for the construction of semantic tools that help specification validation and implementation verification, e.g., through prototyping (specification simulation) and through test case generation, respectively (see Section 5).

Executability is achieved in TRIO along the following lines (details can be found in, [MMG 92]).

A model-theoretic semantics is defined for the language, i.e., an interpretation schema is given that, for any TRIO formula, aims at building possible models of the formula[1].

In general, since TRIO includes first-order arithmetics, the satisfiability of arbitrary formulas (i.e., stating whether or not there exists a model for a formula) is undecidable. Thus, the general interpretation algorithm mentioned above is not guaranteed to terminate with a definite answer.

Partial executability is however obtained by exploiting the idea of finite approximation of infinite domains. Original interpretation domains, which are usually infinite, are replaced by finite approximations thereof. For instance, the set of integers is replaced by the interval [0..1000]. By this way, every decision problem becomes decidable. Of course, there is no a priori warranty that the result obtained in the finite domain coincides with the theoretical result that would be obtained on the infinite domain. In practice, however, one may often rely on this type of prototyping on the basis of experience and common sense.

2.1.1.2 TRIO+: a specification language for complex real-time systems

To support specification in the large, a higher level language, TRIO+, has been defined as an extension of the basic language TRIO [MS94]. TRIO+ exploits the concepts and constructs of the object-oriented (OO) methodology. This is based on the belief that most of OO paradigms are as useful during the specification activity as they are during the design and coding activity. (Perhaps, a specification language should be more supportive of an explorative style than a programming language. In fact, during the coding activity, the programmer starts from a design that should already be well-understood, whereas, during the specification activity, it is more likely that even deep changes occur from one version to another one.) Thus, concepts such as classes, inheritance, and genericity are exploited in TRIO+ and “inherited” from more traditional OO languages.