Abstract
The increasing complexity of embedded systems calls for verification techniques to make sure the systems behave properly. When it comes to safety-critical systems, this aspect is even more relevant and is now taken into consideration by certification authorities. For that matter, property verification is accepted to be done not only on the system itself but also on a representative model of the system. This chapter first introduces the different properties and how they could be expressed. Then associated modeling languages characteristics are discussed to describe the systems on which the properties can be verified. Finally, different technologies to verify the properties are presented, including some practical examples and existing tools. This last part is illustrated by several research projects such as the PRESTO ARTEMIS European project and the exoTICus System@tic Paris Region competitiveness cluster project.
TopProperty Definition
Properties of a system are difficult to define because they either seem obvious, like a plane should fly, or very tricky to explain, like the minimum speed of the plane is relative to its height and weather condition. Generally speaking the properties can be expressed as a set of relations on the inputs and the outputs of the system, or as an evaluation of some internal data in the system. For example a property such as “the speed of the plane should not exceed 900km/h” could be expressed by a mathematical expression such as “system.speed<900” which can be verified automatically by a computer. Usually speaking properties are categorized to be functional or non-functional, and black box or white box.
Functional Property
A functionality is a given scenario of what a system should do; one of the expected behavior. If the system behaves differently it would not mean the functionality is not fulfilled, because all alternative scenarios are not meant to be described for a given functionality. But a functional property describes a mandatory relation between several events. It can be seen as an extension of a function of the system, a piece of scenario that should be verified in any case.
Non Functional Property
A non functional property is generally speaking about the quality level of a property. For example a basic functional property might be that when the button is pressed the light shall lit. A non functional requirement could be that the light should lit within 10mS after pressing the button. Or it could be that the light bulb should have a 10,000 hours lifetime. In a sense a functional property is very straightforward and can be mathematically verified where a non-functional property is more about the quality of a property and is difficult to evaluate. Still one of the verifiable non-functional properties is performance because it is easy to measure, and it can even be estimated with detailed models of the system.
Black Box Property
A black box property is a property that looks at the system as a black box and that only considers what happens on its interfaces. The interest of this type of property is that it can be verified on a real system or a simulated model of the system. The problem is that since the internal information is not visible, to make sure the property is always verified requires all possible surrounding situations to be generated. Without any knowledge of the internal design of the system, the number of possible scenarios might be so large that it might not be possible to explore them all.
White Box Property
A white box property will use the internal information of the system. It is therefore dependent on the system implementation. Verification of a white box property is by construction easier and more efficient but is not always applicable on a real system because the internal information might not be accessible.
Technologies
We will focus on event driven technologies regarding property verification. These technologies apply to communicating system where the possible number of values for the inputs in the system, and the possible sequences of events can create a huge number of different cases for the system. It is therefore interesting to use a model of the system so that the property can be verified on a simulated model.
Key Terms in this Chapter
SDL: Specification and Description Language is an ITU standard used to describe communicating systems.
IMS: IP Multimedia Subsystem is a 3GPP framework designed to deliver multimedia services over mobile networks.
MSC: Message Sequence Chart is an ITU standard to describe interactions between entities.
Formal Model: A model which description is complete and non-ambiguous.
SDR: Software Defined Radio is a technology in which software handles the modulation that was historically handled by hardware.
AADL: Architecture Analysis and Description Language is an SAE specification to describe the hardware and software architecture of a system.
PSC: Property Sequence Chart is a notation to express temporal properties in an MSC or a Sequence Diagrams that is defined by the University of l’Aquila.