Cyrille Comar
email: comar@adacore.com

Robert Dewar
email: dewar@adacore.com

Gary Dismukes
email: dismukes@adacore.com

Certification & Object Orientation: The New Ada Answer

Keywords: Ada, DO-178B, Certification, Object-Oriented Programming

come   L'archive ouverte pluridisciplinaire

Introduction

Software construction has evolved considerably in the last two decades. One of the most notable advances is the use of object-oriented techniques in commercial applications. The enhancement of reusability, adaptability and maintenance has led to wide deployment of these techniques in many application domains.

Languages such as C++, Java, and C# have evolved over the last decade and, thanks to them, object-oriented programming has become a widely used paradigm. Over the same period Ada has evolved to incorporate object-oriented features into its original type model. The Ada 95 standard added to Ada 83 tagged types, single inheritance, polymorphism, and dynamic dispatching. The latest revision of the language, known as Ada 2005, adds multiple inheritance of interfaces and numerous other object-oriented programming idioms.

There is currently a trend towards the use of objectoriented techniques in the construction of highintegrity software systems, such as in avionics airborne systems. In this particular domain, the integration of best practices in software construction must also be balanced with the need to increase confidence in the safety of the system. A further feature to note is that Avionics software has a significantly longer life-cycle than software in other application areas.

The aim of the RTCA DO-178B [START_REF]Software Consideration in Airborne Systems and Equipment certification[END_REF] standard is to provide guidelines for building airborne systems that perform their intended functions with the appropriate level of safety. Developed in the 1980s and finalized in the early 90s, DO-178B is based on the waterfall software process that was considered best-practice at the time the standardization process in this field began. One of the objectives of the forthcoming revision of this standard, DO-178C [START_REF]SC-205, Software Considerations[END_REF] (still in the early stages of development), is to take into account object-oriented techniques and their associated development processes. A preliminary document, the Handbook for Object Oriented Technology in Aviation (OOTiA) [START_REF]Handbook for Object-Oriented Technology in Aviation (OOTiA)[END_REF], already provides a comprehensive analysis and specific guidelines on how to address the safety concerns associated with object-oriented techniques in the context of DO-178B [START_REF]Software Consideration in Airborne Systems and Equipment certification[END_REF].

This paper reviews the most relevant features of the Ada language for certification and summarizes the evolution of object-oriented features in Ada. it then shows how Ada is ideally suited for use in certified applications that use object-oriented features, in particular when complemented with certificationoriented facilities of the development environment.

Ada and Certification

Since the emergence of the RTCA DO-178B standard [START_REF]Software Consideration in Airborne Systems and Equipment certification[END_REF], Ada has been one of the few languages of choice for the construction of airborne systems thanks to its clear semantic definition and strong typing model. It has been used successfully in many major aeronautics projects (Boeing 777, A340, and more recently Boeing 787, A380 and A400M). Clear semantic definition is considered a desirable precondition for minimizing non-determinism by DO-248B [START_REF]Final report for clarification of DO-178B: "Software Consideration in Airborne Systems and Equipment Certification[END_REF] FAQ#32 (What are Defensive practices), where one can read:

Avoidance of non-determinism: Non-determinism may be reduced through one or more of the following practices: 1. Choose a language with a well-defined standard.

Not many languages besides Ada can claim a welldefined official standard. Fewer can claim that all major implementations fully adhere to the standard. And fewer still have an official and standardized test suite [START_REF]Ada Conformity Assessment Test Suite (ACATS)[END_REF] supporting validation of this claim. It is also notable that Ada has several guides for its use in high-integrity systems [START_REF] Iso | Guide for the use of the Ada programming language in high integrity systems[END_REF], [START_REF] Arg | Ravenscar profile for high-integrity systems[END_REF].

Ada's clear semantic definition has also fostered the wide use of ASIS [START_REF]:1999 Information technology --Programming languages[END_REF], which considerably eases the creation of semantics-oriented verification tools. Such tools can be qualified in order to produce evidence that will help meet the DO-178B objective 6.3.4d:

d. Conformance to standards: The objective is to ensure that the Software Code Standards were followed during the development of the code, especially complexity restrictions and code constraints that would be consistent with the system safety objectives.

For example, consider a tool that is part of the standard GNAT toolset: gnatmetric computes industry-standard source metrics such as McCabe cyclomatic and essential complexity [START_REF] Adacore | GNAT Pro User's Guide[END_REF]. Another example is gnatcheck, an ASIS-based tool, whose purpose is to produce certification evidence that specific semantic rules are followed; or when they are not followed, that violations are clearly identified so they can be justified. This tool is designed to be easily extensible for specific project standards. A good implementation will not generate the abortdeferral code that is otherwise mandated by the language. Not only can performance improvements be expected, but more importantly, deactivated compiler-generated code can be reduced, thus easing the effort of code verification and justification for high levels of certification.

There are several interesting subsets of Ada for high-integrity systems. One of them is the Ravenscar profile [START_REF] Burns | The Ravenscar Profile[END_REF], a subset of the tasking features of Ada which is powerful enough for real-time programming but simple enough to be amenable to static analysis for certification, and that can be supported by a small, reliable run-time system. Another notable example is SPARK [START_REF] Barnes | High Integrity Software: The SPARK Approach to Safety and Security[END_REF] that includes Ada constructs regarded as essential for the construction of complex software, but removes all the features that may jeopardize the requirements of verifiability, bounded space and time, and minimal run-time system.

Thanks to Ada's strong typing and subtyping model, run-time checks are generated that can help detect malfunctions earlier, during the testing phase. At high levels of certification, some projects choose not to insert run-time checks in the executable to be certified. This choice can be justified if static analysis tools such as SPARK [START_REF] Barnes | High Integrity Software: The SPARK Approach to Safety and Security[END_REF] have been used to provide proof that specific run-time errors cannot occur. Check elimination can also be motivated by the desire to minimize deactivated compilergenerated code, or by the difficulty of implementing a reliable recovery mechanism, as shown by the Ariane 5 launch disaster analysis [START_REF]Inquiry Board Traces Ariane 5 Failure to Overflow Error[END_REF]:

Although the source of the operand error has been identified, this in itself did not cause the mission to fail. The specification of the exceptionhandling mechanism also contributed to the failure.

Even when compiler checks are not generated in the final executable, they can play a beneficial role, together with pragma Normalize_Scalars ([1] H.1), for satisfying objective 6.3.4f of DO-178B [START_REF]Software Consideration in Airborne Systems and Equipment certification[END_REF] (use of uninitialized variables or constants). Pragma Normalize_Scalars instructs the compiler to initialize scalar variables that do not have explicit initialization with a deterministic value (outside its range when possible), in order to increase the likelihood of generating a repeatable run-time fault when the variable is read before receiving a value. Specific compilers can provide more extensive and comprehensive run-time checks to maximize this possibility. [START_REF] Dewar | Exposing Uninitialized Variables : Strengthening and Extending Run-Time Checks in Ada[END_REF] describes such an implementation and its successful use in an industrial non-safety-critical context (Air Traffic Flow Management). Running a full requirements-based and structural-based testing campaign in such a mode is likely to significantly raise confidence in attaining objective 6.4.3f. For the results of such a process to be acceptable as certification evidence, this compiler functionality does not require full certification since it is not involved in the production of the final code. It only needs to be qualified according to DO-178B section 12.2.2 [START_REF]Software Consideration in Airborne Systems and Equipment certification[END_REF].

Finally, it is worth mentioning that Ada's strong typing system is also known to offer useful capabilities for tools such as static stack-usage analyzers. In particular, [START_REF] Botcazou | Compile-Time Evaluation of Stack Size Requirements with GCC[END_REF] mentions how appropriate type information can be used to compute the maximum stack allocation requirements for variable size objects. It can also help computing complete call graphs even in the presence of indirect calls.

Brief Review of the Ada Object Model

Ada is a general-purpose language that has added support over time for a range of programming paradigms: procedural programming, functional programming, object-based programming, and object-oriented programming with both single inheritance (type extension and dispatching operations in Ada 95) and multiple inheritance (inheritance of interfaces in Ada 2005).

In Ada 83, the object model was limited to data encapsulation and information hiding, using private types and packages to separate specification from implementation. For example, the DisplayElement class of [START_REF]Handbook for Object-Oriented Technology in Aviation (OOTiA)[END_REF] (pp. 3-77) could be represented as: Here the client interface to the Element abstraction is given in the visible part of the package by a private type and a set of operations. The details of the implementation are given separately in the private part and body of the package, effectively insulating the user of the abstraction from the representation and implementation of the type and its operations.

In Ada 95, the language was revised by adding fullfledged object-oriented support in the form of single inheritance, with type extension and dynamic dispatching. This was done in an upward-compatible way, building on Ada 83's existing framework for package encapsulation and derived types. By declaring a type to be tagged and defining a set of primitive operations for the type, the type can subsequently be extended. Such a type extension inherits the data components and primitive operations of the parent type, and can extend the parent type by adding components and operations, as well as by overriding any inherited operations. The notion of type classes was also introduced, to provide polymorphism of objects and operations. Each tagged type T thus serves as the representative root type of a potential hierarchy of the types that extend it, where this set of types is designated T'Class.

The Element abstraction could be represented by the following tagged type: The type Picture_Element is an extension of Element. In this case the new type is declared as a private extension whose full type adds a single new component (hidden from clients of the type). The operation Draw, inherited from the parent type, is overridden by an implementation specialized for the new type (though that implementation might also invoke the parent type's operation). Other operations of the parent type can be inherited as is or overridden, and additional primitive operations can be declared for the type extension (such as the procedure Brighten in this example).

Subprograms declared together with a tagged type in the same package and having at least one parameter (or result) of the tagged type are called dispatching operations of the type. A call to such an operation is not necessarily dispatching however. The call will only dispatch when invoked with an actual parameter whose type is the class-wide type of the associated type class. The first call to Draw from within Draw_Any will dispatch to the appropriate implementation of Draw associated with the underlying value of the parameter X, which might be of any type in the class of types rooted at Element. The second call involves a conversion of the class-wide parameter X to the specific root type Element, and so will directly invoke the procedure Draw associated with type Element (even though the underlying value might be of some other type in the class).

As an extension to the basic capability for type classes, Ada 95 also added a facility for declaring so-called "controlled types". A controlled type allows overriding of three special operations for initialization, finalization, and adjustment (as part of an assignment) of objects. This feature provides the designer of an abstraction with additional control and flexibility in managing objects of the type by ensuring that any resources associated with an object are properly initialized upon creation and cleaned up when the object is no longer needed.

The most recent revision of the language, known as Ada 2005, introduces several new capabilities that enhance the existing object-oriented features. These include:

• the ability to conveniently define mutually dependent types in separately compiled packages (limited with clauses) Textual_Element derives from Element and thus inherits its primitive operations. It can override some of them, such as Draw, as well as define new ones, such as Get_Displayed_Value. The keyword overriding makes the choice clear to the reader and allows the compiler to detect inadvertent typos that could otherwise be interpreted as overloaded operations.

Ada 2005 also introduces the conventional object prefix notation for invoking operations on objects, permitting programmers to use object.method (param); as an alternative to the Ada 95 functional form method (object, param);, as illustrated by the following calls: X.Draw; Put_Line (X.Get_Displayed_Value); Finally, Ada 2005 introduces a Java-like limited form of multiple inheritance through the keyword interface.

The interface feature enables inheritance of specifications (roles) rather than implementations, avoiding the complexity and danger of the more general forms of multiple inheritance.

An interface as defined in Ada 2005 is very similar to an Ada 95 abstract tagged type which has no components and each of whose operations is either abstract or null. The type extension rules are enhanced to allow tagged types (as well as interfaces) to inherit from any number of interfaces. In order to preserve single inheritance of implementations, a tagged type extension must still derive from a single tagged type ancestor. When a tagged type inherits from one or more interfaces, it must override any abstract operations inherited from those interfaces (unless the tagged type itself is abstract).

Simple Object Model (without Dispatching)

In their current form, certification standards such as DO-178B [START_REF]Software Consideration in Airborne Systems and Equipment certification[END_REF] are wary of dynamic dispatching. If its use is not formally banned, it is strongly discouraged by the afore-mentioned FAQ 34 in DO-248B [START_REF]Final report for clarification of DO-178B: "Software Consideration in Airborne Systems and Equipment Certification[END_REF] which explicitly states:

Avoidance of non-determinism: Non-determinism may be reduced through one or more of the following practices: … 4. Avoid use of dynamic binding…

Dynamic binding is a synonym for dispatching (see [START_REF]Handbook for Object-Oriented Technology in Aviation (OOTiA)[END_REF] 1.3.5). Non-determinism introduced by dispatching will be discussed in the next section along with issues related to proper testing of such constructs. Although solutions to these issues are emerging, they are not yet fully established. The same wariness caused dispatching to be excluded from the first version of the Ada standard. Now that a complete object-oriented paradigm is supported in Ada, the question arises: can it be of any use to those who prefer not to have to deal with the certification difficulties related to dispatching? Ada's answer is clearly "yes". Type extension and inheritance are powerful mechanisms for defining closely related abstractions and can be used without dispatching.

The "object.method" notation is also considered a significant syntactic improvement in some situations, particularly when it simplifies the source code and thus enhances its readability. This is especially true where local coding standards prohibit use clauses. This is the case in SPARK [START_REF] Barnes | High Integrity Software: The SPARK Approach to Safety and Security[END_REF], which requires that any entity always be referenced using exactly the same syntactic form thus entailing the use of fully qualified names. When a method defined in a different package is called on a local object, the difference of notation can result in substantial simplification: In Ada 2005, this prefixed notation is only available for primitive or class-wide operations of tagged types, which encourages their use even when dispatching is prohibited. Such a prohibition can easily be enforced by using the standard restriction:

Pragma Restrictions (No_Dispatch);
This is a configuration pragma applying to all units in a partition. Such a restriction can also be used by certification-friendly implementations to avoid generating all the implicit code required to support dispatching properly. For instance, the so-called "tag" component no longer needs to be materialized in tagged records. Dispatch tables do not need to be generated, nor filled during type elaboration. Implicit dispatching operations such as "=", 'Size, 'Read, and 'Write can be avoided. These operations usually need to be created unconditionally for each tagged type, in order to support potential dispatching calls from different units. Such simplification of the generated code reduces the need for localizing and potentially needing to justify deactivated compiler-generated code as already alluded to in section 2.

Towards Certification of Dispatching Calls

Section 3 showed that the programmer can choose whether a given call to a primitive operation will dispatch. This flexibility can be used to limit the number of dispatching calls, thereby limiting their associated certification cost. This flexibility is not available in Java, where all operation invocations are dispatching (unless a routine is declared as finalsimilar to an Ada class-wide operation). It is available in C++, but at the cost of forcing the programmer to indicate whether an operation itself (not a specific call) is virtual. A virtual operation will potentially always dispatch while a non-virtual one will never dispatch. C++ implementations are allowed to optimize dispatching calls into regular calls when the context permits, but this is not under the control of the developer.

It is also worth noting that most OOTiA [START_REF]Handbook for Object-Oriented Technology in Aviation (OOTiA)[END_REF] guidelines in 3.3 (Single Inheritance and Dynamic Dispatch) are easily met when using Ada 2005:

• the Simple Overriding rule and the Simple Dispatch rule are guaranteed by the language • the Accidental Overriding rule can be met by systematic use of the overriding keyword (this again can easily be checked with an ASIS tool) • the Dispatch Time rule is a characteristic of the implementation that can be expected to be met provided that the semantics of the language allow constant-time dispatching through compiler generated dispatch tables.

It has often been observed that dispatching calls are equivalent to case statements. This is of course not the case at the conceptual level of the application developer, since the point of using dynamic dispatching is that the programmer invoking an operation at any particular point does not need to know the set of possible method destinations. In fact nowhere in the entire source set does anyone have to know the set of destinations. That is at once the strength and weakness of the dynamic polymorphism model. The programmer does not know what the flow of control will be, and the flow of control is not known until run time. This is true for all conditional constructs. What distinguishes the dispatching case is that the programmer does not even know statically the set of possible control flows. Since an important element of certification is static testing of all possible control flow paths, there is a fundamental contradiction between the aims and requirements of the programmer at the source level, and the aims and requirements of certification. Dispatching is all about not having to know the possible control flow. Certification is all about needing to know it.

However, once a program has been written, there are indeed transformations that can convert dispatching to the equivalent of case statements. These transformations can be implemented as source-to-source transformations, or can be performed as linker-level activities. We will describe the transformations in terms of source rewrites. The first step is to observe that although during the writing of any particular component of the program, the final set of possible destinations of a dispatching call is unknown, this set is well known by the time the program is linked.

In this discussion we assume that a static linking step produces the executable for a given program. If we consider the realm of highly dynamic object oriented environments which are common with Smalltalk or Java, but can also exist in Ada (see [START_REF]:1999 Information technology --Programming languages[END_REF]), where new classes can be introduced during the execution of the program, then the situation is much more difficult. We do not attempt to address the issue of certification in such environments. Given that we know the possible set of destinations, the idea is to replace a dynamic call:

Object.Operation; by a proper Ada case statement case Object'Tag'Index is when Subtype1'Tag'Index => Subtype1 (Object).Operation; when subtype2'Tag'Index => Subtype2 (Object).Operation; … when others => raise Program_Error with "invalid tag"; end case;

Here the calls are not dispatching since the Object is converted to its actual subtype. The set of possible cases is complete since such a transformation is done with a view of the entire program.

There are two ways to replace dispatching calls with case statements. First, we can directly replace each call by such a case statement. Hence, if there are multiple calls to the same operation there will be multiple case statements. Second, we can make a single procedure containing the case statement, and then replace each dynamic call with a call to this procedure.

OOTiA [START_REF]Handbook for Object-Oriented Technology in Aviation (OOTiA)[END_REF], in section 3.12.5, provides a good discussion of the amount of testing required for adequately covering dispatching calls. It proposes four possible levels of coverage. The most stringent is equivalent to traditional covering of the first suggested transformation, that is to say, covering all methods that can be dispatched to at all call points. It is considered a "pessimistic approach" and would probably generate an immense burden on applications that use dispatching extensively. The most optimistic approach is equivalent to the coverage of the second transformation. It is considered to be a relatively weak approach to testing for safety-critical applications. Intermediate approaches based on mathematically significant subsets or equivalence classes amount to selectively using one or the other transformation. At the time of writing, the most fitting approach remains open. Specific guidelines are expected to appear as part of the current work on DO-178C [START_REF]SC-205, Software Considerations[END_REF].

Note that doing an actual transformation of the code into case statements (rather than just arguing for equivalence at a tool level) offers substantial advantages. First, the usual implementation of dispatching is to issue an indirect call. This means that if the tag of an object is corrupted, we get a worst case erroneous execution involving a random jump. For a case statement, if the tag is corrupted, the effect is much more strictly bounded, since the "when others" branch is taken and a well-known error condition is raised. Second, case statements are known constructs, completely familiar to existing tools for producing certification evidence in non-OO contexts, so the potential for reuse of such toolsets without substantial redesign is attractive.

An enhancement planned for GNAT will implement both schemes for rewriting case statements. The way this will work is that there will be a compiler option to generate appropriate calls, and a binder option to generate the source of the case statements (one per call, or one per operation, depending on the option chosen). These will be generated as normal Ada source and will therefore be fully processable by any normal tools, including the debugger and certification tools. Comments added to generated case statements will provide traceability back to the original calls in the application source units.

What about Multiple Inheritance?

OOTiA's [START_REF]Handbook for Object-Oriented Technology in Aviation (OOTiA)[END_REF] purpose is to define a safe path for the introduction of OO techniques in safety critical software. As shown in previous sections, safety issues related to single inheritance, especially in strongly typed languages, are relatively well understood and are amenable to known and proven approaches. On the other hand, the document is much more circumspect with respect to multiple inheritance and hints several times at doubts as to its usability in a safety-critical context. See, in particular, section 2.3.1.3: …. For example, ANSI C++ has some language features, such as multiple inheritance, that may make it difficult to meet some DO-178B objectives….

However, OOTiA makes a strong distinction between multiple inheritance of implementation as provided by C++, and delegation, or interface inheritance as is provided by Java and Ada 2005. If the avionics community does not seem ready to go so far as to allow the former, the secure use of the latter does not seem out of reach. See for instance 3.4.3: Although use of these guidelines helps us deal with the issues raised with respect to ambiguity and complexity, delegation is still considered preferable to the use of multiple implementation inheritance for most systems (as recommended by the AVSI Guide [START_REF] Avsi | Guide to the Certification of Systems with Embedded Object-Oriented Software[END_REF]).

One of the major guidelines in [START_REF]Handbook for Object-Oriented Technology in Aviation (OOTiA)[END_REF] is the repeated interface inheritance rule, whose intent is to avoid potential ambiguities introduced by inheriting the same operation from different parent interfaces. This condition is guaranteed by Ada 2005 semantics. The other guidelines related to multiple inheritance of interfaces are either not relevant to Ada or can be easily checked by ASIS-based tools such as the ones mentioned in section 2. Therefore, this is another domain where Ada provides what seems to be the appropriate level of support for a feature that may become accepted in safety-critical contexts in the not-too-distant future.

Conclusion

The latest revision of the Ada language includes a complete scalable object-oriented model that mixes well with Ada's strong typing tradition. This model is well suited to answer the challenge of introducing various object-oriented techniques into the development of applications requiring various levels of certification. Its most restricted object model can be used with today's most strict certification practices. If dynamic dispatching creates difficulties with current certification practices, Ada is well positioned to offer safe alternatives to overcome those difficulties.

Acknowledgement

Many thanks to John Barnes, Kathy Fairlamb, Ed Falis, Jose Ruiz and Ed Schonberg for their invaluable reviews and comments.

  Parent.Child.Grandchild.Method (Obj, Param); compared to the much simpler: Obj.Method (Param);

pragma Restrictions (No_Abort_Statements); pragma Restrictions (Max_Asynchronous_Select_Nesting => 0);

	no cycles in the subprogram call
	graph).
	Ada's pragma Restrictions ([2] 13.12) is also a
	significant aid for enforcing the "Conformance to
	standards" objective mentioned above. For instance,
	dynamic memory allocation, whether implicit or
	explicit, can be excluded from the application by
	simply specifying:
	pragma Restrictions (No_Allocators);
	pragma Restrictions
	(No_Implicit_Heap_Allocation);
	Furthermore, the compiler can take advantage of
	pragma Restrictions to produce simpler and more
	efficient code. For instance, in the presence of

It already implements dozens of local rules, such as "no goto statements" as well as several more global ones such as "no side effects in functions" (i.e., no direct or indirect modification of a variable whose scope is wider than the function body) and "no recursion" (i.e.,

  The keyword tagged in the declaration of type Element identifies the type as being extensible. Element is the root type of a class of types that could be derived from it, while Element'Class denotes the entire set of types in that class. The type Element can now be extended, for example by defining a specialization:

	package Pictures is
	type Picture_Element is
	new P.Element with private;
	procedure Draw (X : Picture_Element);
	procedure Brighten
	(X : Picture_Element; Y : Intensity);
	... private
	type Picture_Element is new P.Element
	with record
	Brightness : Intensity; end record;
	end Pictures;

package P is type Element is tagged private; subtype Any_Element is Element'Class; procedure Draw (X : Element); … end P;

Glossary


Dr Meinhard Erben

Dr Wolf Günther

Dr Tobias Sedlmeier

Dr Dieter Lederer

Dr Klaus-Jürgen Amsler

Legal Aspects of Safety Designed Software Development, Especially under European Law

Keywords: Software development, product liability, producer's liability, compliance with safety standards, IEC 61508 1

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The use of software in automobiles and other means of transportation increases rapidly. 1 As softwareunless it is completely trivial -cannot be developed without defects, the number of software defects in electronic controller units (ECU) used in automobiles and other means of transportation increases as well, leading to malfunctions and failures of electronic systems. Defects in safety relevant applications such as driver assistance systems (steering, brakes etc.) may have disastrous impacts on the OEM as well as on the suppliers: Defective software may not only cause personal deaths or injuries, but it may also result in recall actions, producing high costs and resulting in heavy burden on the image of all the companies involved. In Europe, product liability generally applies regardless of any fault of the manufacturer, with only one exception, i.e. if the relevant product's defect was inevitable.

Due to these facts and since risks arising from a legal conflict in connection with statutory or contractual liability are more than costly, there can be no reasonable doubt that it is advisable to treat the subject of safety designed development processes with utmost care. In this lecture, we shall outline the potential warranty and liability risks under European law regarding defects in software, and we shall then present a composition of the necessary organizational and legal measures regarding contract and project management, in order to prevent the realization of these risks to the extent possible.

2.

Basic Legal Principles Regarding Defective Software

"Defect" in Terms of Law

The supplier is basically only liable to its customers or to any third party, in case its product contains a defect in terms of law. Therefore, the term "defect" is the central term within the framework of warranties and/or liabilities. In order to decide which measures must be taken to ensure that the development process of software and/or the software products resulting from this process do not contain a defect in terms of law, we shall first take a closer look on the legal definition of "defect".

Features Agreed on in the Contract as Defect

Where the parties have agreed on certain specifications of the contractual software, the software is defective in terms of law:

• If it does not comply with the specifications agreed between the parties,

• -In case there is nothing provided for in the contract: If the software does not contain such features necessary for the use of the software that can generally be expected from a software falling into the same category as the software agreed on in the contract, or

• If it does not contain such features which the customer could have reasonably expected with respect to the specific software or with respect to the agreements relating thereto.

Obviously, the customer will expect the software to have such features, which are expressly agreed on in the contract. As simple as this may sound, these expectations are often the basis for legal conflicts, since it is often unclear, what exactly the parties meant by certain wording and/or language in the contract in connection with the description of the software's specifications. If such questions are in dispute, the courts have to decide on the conflict in accordance with the common legal interpretation rules. This interpretation will, under most European laws (e. g. German law), take into account the principles of good faith from an objective point of view, considering specific practices of the parties' profession.

Example: If it is agreed that "the software shall have appropriate response times", such response times are different with respect to call center software or with respect to software for the automotive industry, and they are also different depending on the scope of the specific task.

Features not Expressly Agreed on in the Contract as a Defect

To the extent the parties have not expressly agreed on specific features in the contract, the software must -according to Article 6 of the European Directive 85/374 EEC -contain such standard specifications, which can reasonably be expected by an average market participant. What exactly such a participant is allowed to expect depends on the conceivable use of the software. Such use does not only contain the features the manufacturer intended, but also those functions which an average market participant usually expects from the product.

To comply with these possible expectations regarding safety specific defects:

• The software has to be designed and manufactured in accordance with the current standard of science and technique (= state-ofthe-art techniques), as well as with the common use of the product usually applied by the relevant professions. 2

• Furthermore, the software has to be as safe and secure as the customers (i.e. the public) can reasonably expect with respect to the software's common application areas. 3

• In addition, the customer's expectations are legitimately influenced by the price range of the product. For example, a luxury car can be expected to have more safety-designed features than a lower middle class car. Or, another example, in the year 2000 the customer could, from a legal point of view, not have reasonably expected that a middle class car is equipped with an ABS-system [START_REF] Bodewig | Der Rückruf fehlerhafter Produkte[END_REF] .

Now we know what a "defect" is. So let us now deal with the question, in which cases the producer can be held liable for such a defect.

Liability Risks Arising from Defective Software

Under European law, two areas of liability risks have to be distinguished in connection with defective software. One arises from the contractual obligation vis-à-vis the contractual partner to deliver a nondefective product (contractual warranty and liability), and the other results from the statutory obligation to prevent the customer from damages to his property and from personal damages by distributing safe and secure products (so called "product liability" and "producer's liability").

Contractual Warranties and Liabilities

Under to the European Consumer Sales Directive 1999/44/EG, the distributor has to deliver nondefective products. In various EU member states, the tight rules of the Consumer Sales Directive have not only been implemented with respect to contracts with consumers, they have in fact also been implemented with regard to all other kinds of contracts. One provision of this Directive states that, if the product is not free of defects, the customer may claim the remedy of the defects or the substitution of the defective product by a nondefective product, both during the warranty period of two years. This warranty period of two years is mandatory with respect to contracts with consumers. Customers may exercise the before mentioned rights regardless of whether the defect was caused by the distributor's fault or not. However, if the defect was caused by the distributor's fault, the customers may additionally claim compensation for damages caused by the use or the uselessness of the defective product, such as damages to objects other than the defective product, loss of profit, etc.

Statutory Liability

Both legal concepts of statutory liability -product liability as well as producer's liability -are based on the idea that a producer, and, under certain conditions, also the distributor of a product shall advert damages from the property and the persons of the product's users by making the product as safe as technically possible. • The development and/or the design of the program (causing the occurrence of the defect in each single exemplar of the series),

• The manufacturing the product (i.e. the defect can only be found in the product affected by the manufacturing error), or

• An incorrect instruction with respect to the product (i.e. the product itself is not defective, but the manual or user documentation leads to an incorrect application of the product). Please note that according to the jurisdiction of many European countries (e.g. the jurisdiction of Germany), software manuals are part of the product, which means that if the manual is defective, the software itself will be considered to be defective. Since software defects are by nature defects in the development and/or design, the fulfilment of the organizational requirements of the producer/manufacturer in connection with the development and/or design process is the core instrument to prevent warranties and/or liability claims. Therefore, the non-compliance with safety oriented laws, statutes and/or technical standards is a clear fault in the development and/or design process of the software, regardless of whether this has been expressly agreed on in the contract or not.

Evidence Rules

All these liability concepts (contractual warranty and liability, product liability and producer's liability) have one thing in common: A successful defence against claims for damages requires the producer and/or distributor to be prepared to prove that he has undertaken anything possible to produce the relevant software without defects. This must be kept in mind, since many legal proceedings are decided on the basis of evidence rules. The loss of a lawsuit regarding claims for damages for defects in safety relevant applications can be crucial to the manufacturer.

Contractual Liability

For a successful assertion of contractual damage claims relating to defects in software, the claimant has basically only to expose and -in case of a contradiction of the opponent -to prove that his damage was caused by a defect of the relevant product and that the claimed defect has originated in the sphere of the contractual partner. The contractual partner is only able to repel the claim if he can prove that the defect was not caused by his negligence. In case the manufacturer itself has distributed the software to the claimant, he has to prove that he has undertaken anything possible and reasonable to avoid the formation of defects during development, production and delivery of the software. This implies the application of quality assurance measures which match the current stateof-the-art methods and technologies. If the software was not distributed by the manufacturer but by a (pre-)supplier, the supplier has to prove that he has taken any possible and reasonable measures to detect the defect before delivery. Therefore, the supplier as well has to apply all state-of-the-art test procedures and logistics systems. All these quality assurance measures and their application have to be reasonably documented in case they need to be presented in a legal conflict.

Product Liability and Producer's Liability

With respect to product liability and producer's liability the burden of proof is similar as under contractual liability, since the customer usually is not in a position to analyze the design, development and production or distribution procedures of the manufacturer: Once again, the customer has basically (only) to expose and to prove that his damage is a result of a defect in the software and that this defect has originated from the manufacturer's sphere of responsibility. It is then the producer's burden to disprove this allegation. Such allegation can only be successful if the producer maintains and controls the conformity with adequate quality assurance systems and the documentation of such measures. Before taking a closer look at which quality assurance systems constitute an adequate safety orientated development process, let us deal with the question, of whether the compliance with applicable safety norms is sufficient to exclude the manufacturer's liabilities.

Does Compliance with Applicable Safety

Norms and/or State-of-the-Art-Techniques such as IEC 61508 Result in an Exemption from Liability with respect to the Producer and/or Supplier?

It has already been stated that, on the one hand, the producer is obliged to comply with all applicable technical norms, as well as with all applicable laws or statutes regarding the fulfilment of such obligations which apply in order to protect the safety of the general public. If he fails to do so, this would be a clear fault in the design and/or development process of the software. On the other hand, however, the compliance with all applicable safety norms and/or state-of-the-arttechniques such as IEC 61508 does not result in an exemption from liability with respect to the producer and/or supplier. We would like to emphasize this point very clearly: The compliance with all applicable safety standards such as IEC 61508, the European Directive 2001/95/EG concerning Product Security and its national transpositions (e.g. the German Product Security Act = GPSG 6 ) determine only the minimum standard the customer may expect from the products, i.e. compliance with these norms is not sufficient to exclude nor to limit the producer's liability. In practise, this means that the adherence with all statutory laws and safety standards is only circumstantial evidence that the product complies with the state-of-the-art techniques. [START_REF] Cf | Sicherheitsgerechte Entwicklungsprozesse (Safety-Designed Developing Processes)[END_REF] If the technical progress has gone beyond these norms or if the use of the product reveals new potential risks or dangers, the development and manufacturing process has to be adapted to such new requirements. 8 In effect, this means that the compliance with all applicable safety norms and/or state-of-the-art-techniques such as IEC 61508 may not be sufficient to prove that the manufacturer has in fact been faultless for a defect in the product.

Legal Measures for the Fulfilment of the Manufacturer's Organizational and Due Diligence Obligations

What can, shall and/or must be done in terms of law to be as much on the safe side as possible?

The conclusion of the considerations so far is that one core instrument for a successful defense against contractual and statutory claims relating to product defects is a standardized project management taking into account all necessary organizational and legal requirements to achieve the following goal of the design and development process: A "non-defective product".

Organizational Requirements

The goal: "non-defective product" is inseparably linked to the organization of the design and development, the production as well as the distribution process. It has to be ensured that this process is organized in such a manner that all stateof-the-art measures and technologies are complied with. This requires, among other things, at least the following measures:

• Pre-supplier products have to be tested, unless the pre-supplier is able to prove that he has the relevant know-how to test the products itself and that he has in fact carried out all required tests. 9

• The producer has to monitor its products after the distribution, to be able to detect possible defects which have remained undetected during the development and manufacturing process.

• The development process has to be structured with a clear phase scheme and milestones.

• The application of and the compliance with the organizational measures have to be documented and saved so that they can be accessed and provided in the event of a legal conflict. We strongly advise to comply with all applicable safety norms and state-of-the art-techniques for another reason: It is a pre-condition for the producer to be able to prove that the manufacturer or supplier has indeed complied with all applicable norms, and not only claims to have done so. Since, in the event of occurred damages, some European (e.g. the German) courts oblige the producer to exculpate itself from the allegation of negligent behavior 10 the manufacturer is well-advised to implement and to control the adherence with a quality system by which he can effectively prove that he has indeed complied with all applicable norms and standards in each phase of the development and manufacturing of the software.

• When developing embedded systems, the manufacturer has to fulfil additional requirements, since embedded systems are highly complex systems. Since software cannot be developed without defects, [START_REF] Cf | Sicherheitsgerechte Entwicklungsprozesse (Safety-Designed Developing Processes)[END_REF] the project management must include and take into account all the requirements for hardware and software in parallel environments including all necessary concepts for the design, implementation, testing, integration and simulation processes. Thus, an effective risk management, risk control procedures and a comprehensive configuration management are minimum obligations the manufacturer has to comply with.

4.2

Requirements Concerning Contractual Management What needs to be done from a legal point of view regarding the contractual management?

• We strongly advise that any manufacturer of products in safety relevant applications shall set up an effective project as well as contractual management. This starts out with a clear contractual framework, including legal specifications of relevant terms for the development process. It then includes clear and realizable specifications for the acceptance of the performances, including test specifications and acceptance criteria. It also includes a clear, realizable and verifiable process for change requests occurring during the development process. And it also includes a clear specification of when exactly which version of the product has been delivered, including a documentation of whether the delivery has occurred for testing purposes only or whether the release is the final, completely tested and released version which shall go into production in serial products.

• The contractual management shall be designed in such a manner that it defines a "legal environment" in which product defects and discussions of whether a product defect has occurred are prevented to the extent possible. Phase building, clear, complete specifications, clear change request procedures, test criteria, acceptance criteria as well as the compliance with all of the above are only some of the essential measures necessary to achieve the sub-ordinate target of a successful contractual and project management, on the way to the final aim: "non-defective product".

Implementation of the Organizational and Legal Requirements

For safety related systems IEC 61508 is an international generic standard. For the automotive industry it is a main standard until there is an automotive specific adaptation. The development of an ISO norm based on IEC 61508 is in process but available probably not before 2008 [START_REF] Amsler/Erben | Über Prozessreife zur Sicherheitsintegrität (Safety Integrity Based on Process Maturity)[END_REF] . Although being vague in some requirements, IEC 61508 is nevertheless a helpful means to fulfil the organizational and legal requirements, because the standard is a comprehensive survey of requirements regarding the development of safety related systems.

Part 1 to 3 13 define the main requirements addressing document management, (organizational) requirements for the management of functional safety, the institutionalization of a safety life cycle and safety assessments. In addition, there is a catalogue (part 7) with well known methods and techniques that are recommended to be applied to ensure the safety integrity of systems. On the other hand, a direct implementation of the requirements of IEC 61508 is very difficult because it is a hefty and complex tome without any hints how to implement its requirements. Although defining a safety life cycle comparable to the V-Model 14 the structure of IEC 61508 is not process oriented. It is rather a bundle of requirements assigned to the phases of the safety life cycle. When trying to implement these bundles of requirements there will be the risk to take only single measures which are not coordinated and therefore may be of little efficiency from an overall process point of view. The recommended way for implementing IEC 61508 is applying a process management approach based on maturity models like CMMI or ISO 15504 (SPICE) 15 . Maturity models incorporate accepted best practices and provide a structured process framework that supports an efficient way for improving process maturity step-by-step and therefore to improve the transparency of processes, the traceability of any product changes and the integrity of the work products. All of the above support the development of non-defective software.

Comparing the requirements of IEC 61508 with the Process Areas and Specific Practices of CMMI goes to show that the Process Areas representing a Maturity Level 3 are a very good basis for implementing a development process that conforms to IEC 61508 [START_REF] Amsler/Erben | Über Prozessreife zur Sicherheitsintegrität (Safety Integrity Based on Process Maturity)[END_REF] . Some safety specific requirements of IEC 61508 like e.g. performing hazard analysis can be considered as safety specific adaptations of Specific Practices of CMMI, in this case a specific application of the Risk Management Process Area.

Increasing the Safety Integrity Level (SIL) for a product also increases the requirements for the development process regarding the methods and techniques to be applied. According to IEC 61508-2 e.g. statistical testing should be applied for SIL3 products. In addition, with increasing the Safety Integrity Level of a product the requirements regarding the efficiency of applied methods and techniques will also increase, from low, medium to high efficiency.

Both SIL dependent requirements can be fulfilled with increasing the process maturity by applying maturity models based on CMMI or ISO 15504. Maturity models like CMMI or ISO 15504 are therefore a smart and efficient approach for implementing requirements of IEC 61508 and to fulfil the organizational and legal requirements.

Summary

The implementation and application of procedures described in applicable safety standards such as IEC 61508 are core pre-conditions in order to prevent liability risks applicable under European law with respect to defective software.

  Product liability and producer's liability coexist independently. The major difference between both legal concepts is that product liability applies regardless of whether the product user's damages were caused by the producer's fault or not.

	Neither product liability nor producer's liability covers
	financial losses. In fact, both concepts only apply
	with respect to damages to products and with
	respect to injuries of persons.
	2.2.2.1 Product Liability
	Product liability applies in cases in which a defect of
	a product leads to damages, regardless whether the
	manufacturer is at fault or not. The only exception
	therefrom is set forth in Art. 7 lit. e of the European
	Directive 85/374 EEC: Product liability is not
	applicable if the defect of the product could not have
	been prevented even by using state-of-the-art
	technologies at the time the product has been sold.
	As almost all defects of products are technically
	avoidable, product liability will apply in almost all
	cases in which a product contains a defect.
	Therefore, from a legal point of view, product liability
	may only be avoided with respect to the end product
	by preventing defects in the course of the design
	and/or development process.
	This is one reason why a safety designed
	development process must be implemented into the
	organizational structure of any entity dealing with the
	design and development of products, in particular
	dealing with the design and development of software
	which is used in safety critical application areas.
	2.2.2.2 Producer's Liability
	Producer's liability means liability for defects caused
	by:

The legal concept of "producer's liability" has been developed by European courts as case law based on the principles of tortious liability. This development has already taken place before the European Directive 85/374 EEC and its national implementations (e.g. in Germany by the Product Liability Act (PHG) 5 ) came into effect. This directive contains the European statutory framework for the legal concept of "product liability".

Cf. Schelling/Fetzer/Erben, "Software-Komponenten, Ein


John Rushby

Formal Analysis for Embedded Real-Time Systems

Keywords: formal methods, model checking, automated verification

Timed systems are notoriously hard to debug and to verify because the continuous nature of time allows vast numbers of different behaviors; embedded systems must often deal with faults, and these introduce another dimension of complexity. Simulation and testing provide little assurance in these domains because they can visit only a small fraction of the possible behaviors. Formal methods of analysis have some promise, but until recently they could deal only with one dimension at a time: classical model checking could cope with faults but could not model continuous time; model checkers for timed automata could deal with continuous time but not the "case explosion" due to faults. Recently, a new class of "infinite bounded" model checkers has been developed; these show promise that they can cope simultaneously with both continuous time and discrete faults.

Introduction to Model Checking

Computer systems are hard to debug and to verify because the presence of decision points in the flow of control introduces discontinuous behavior: we cannot assume that "nearby" inputs and states should produce "nearby" outputs-and hence there is no justification for extrapolating from tested cases to untested ones. In the absence of continuity, the only way to fully analyze the behavior of a computer system is explicitly to consider every case (either by testing or by reasoning). This is infeasible in general, but when the state and input variables range over fairly small discrete sets of values there is a technology called "model checking" that can consider every case. The simplest form of this technology is an explicit state model checker: this is like a simulator for the programming or modeling notation employed, except that it records every state (i.e., assignment of values to state variables) encountered, explores all the successors to each state (by considering all possible assignments to input variables and by resolving nondeterminism in all possible ways), and thereby systematically explores the entire space of reachable states. A model checker can verify that a given predicate is satisfied in every reachable state (e.g., "at most one process is in its critical region"), and it can verify more complex properties (e.g., "every request is eventually followed by a grant") specified in a property language that is usually based on some form of temporal logic. When a property is violated, the model checker can construct a counterexample, which is an explicit scenario leading to the violation. A modern explicit state model checker such as SPIN [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF] typically can explore tens of millions of reachable states in an hour or so. On the other hand, symbolic model checkers based on BDDs (reduced, ordered Binary Decision Diagrams) can often explore systems having 10 200 states in a few hours. As the name suggests, this class of model checkers represents states and programs symbolically: this is generally more compact and efficient than explicit representations (for example, the set of explicit states {(0, 1), (0, 2), . . . , [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Barrett | SMT-COMP: Satisfiability modulo theories competition[END_REF], (1, 3), . . . [START_REF] Barrett | SMT-COMP: Satisfiability modulo theories competition[END_REF][START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF], [START_REF] Barrett | SMT-COMP: Satisfiability modulo theories competition[END_REF][START_REF] Cimatti | NuSMV: A new symbolic model verifier[END_REF], . . .} can be represented symbolically as {(x, y) | x < y}). NuSMV [START_REF] Cimatti | NuSMV: A new symbolic model verifier[END_REF] and SAL [START_REF] De Moura | SAL 2[END_REF] are examples of tool suites that provide symbolic model checkers. Bounded model checkers also use a symbolic representation, and originally were specialized for finding counterexamples: given an explicit bound (hence the name) a bounded model checker decides whether there is a counterexample to the specified property that is no longer than the bound. Bounded model checkers use SAT solvers (tools that solve satisfiability problems for formulas in propositional logic) as their underlying engines; although SAT is the quintessential NPcomplete problem, modern SAT solvers are very effective and bounded model checkers can often handle larger systems than symbolic model checkers. There are a several methods for extending bounded model checking from refutation (i.e., looking for counterexamples) to verification: one such method is k-induction (where the bound k is a small integer), which is a generalization of ordinary induction (which is 1-induction in this framework). NuSMV and SAL both support bounded model checking and k-induction. Model checkers have their own idiosyncratic system specification and property languages. Given a system description in some other notation, it is first necessary to translate it into the language of the model checker concerned: there are several translators from model-based design notations into the languages of various model checkers. Next, the requirement must be formulated in the property language of the model checker; alternatively, the system description can be augmented with a monitor that raises an error sig-nal when a requirement is violated and the model checker is then given the property "always not error." Finally, the chosen model checker can be invoked; these usually have several command line options (e.g., the bound to be used in bounded model checking) but their actual operation is automatic. The possible outcomes are that the property is verified, or it is refuted and a counterexample is provided (which may need to be translated back to the notation of the original system description), or the model checker exhausts memory or time (or the patience of its user). In the latter case, it may be necessarily to downscale the system description (i.e., to chop down the size of its data structures or other variable parameters, or to simplify it in other ways), or to abstract it (a more principled form of simplification). Excessive simplification may lead to false counterexamples, which can then suggest how the simplification can be made more precise: this process is automated as "counterexample guided abstraction refinement" (CEGAR) in software model checkers such as BLAST [START_REF] Henzinger | Software verification with BLAST[END_REF]. There are many examples of successful industrial application of model checking to embedded and other systems, for example [START_REF] Miller | Proving the shalls[END_REF]. Experience indicates that we can learn more (and find more bugs) using model checking to examine all the behaviors of a possibly simplified model than we can by testing just some of the behaviors of the real system.

Discrete Time

It is easy to extend model checking to timed systems when activities are synchronized to a global clock that provides discrete "ticks," as in hardware circuits. We simply add the clock to the system description and specify properties in terms of elapsed clock ticks: e.g., "every request is followed by a grant after at least 3 but no more than 7 ticks." In the simplest models, the clock advances by one tick in every step and other components sit idle until it is time for them to do something. A model checker may then need to go infeasibly many steps deep to verify or refute a property. An alternative approach has each component indicate the number (which may be nondeterministically determined) of ticks into the future when it will next do something. The clock can then advance time all the way to the earliest such "timeout"; that component then performs its action and sets its next timeout. The modeled behavior thus alternates between component actions (there may be several components waiting on the same timeout) and the clock advancing time to the next timeout. This modeling approach using timeout automata was developed by Dutertre and Sorea [START_REF] Dutertre | Timed systems in SAL[END_REF] for continuous time, but Lamport uses a similar approach for discrete time [START_REF] Lamport | Real-time model checking is really simple[END_REF]. In some applications, the regular ticks of a discrete clock can be replaced by irregular events: rather than the clock generating ticks that are received by other components, the components generate events that are perceived by some observer and we count how many events arrive until some interesting state is achieved. If events are related to clocks local to each component, then we may be able to verify timed properties of asynchronous systems. This is done, for example, in analysis of the startup protocol for the Time Triggered Architecture (TTA) [START_REF] Steiner | Model checking a fault-tolerant startup algorithm: From design exploration to exhaustive fault simulation[END_REF], where we are able to verify that a 4-node TTA cluster will always start up within 23 TDMA slots; by varying the bound, we are able to show that 23 is indeed the worst case.

Continuous Time

While discrete time is appropriate in some circumstances, accurate modeling of most real-time systems requires that time is treated as a continuous variable. This takes us out of the realm of classical model checking because continuous variables can take an infinite number of values and therefore lead to an infinite state space, whereas classical model checking depends on explicit or symbolic enumeration of a finite state space. Of course, the continuous nature of time also makes real-time systems very hard to design and to test, and therefore makes some kind of automated analysis all the more desirable. Fortunately, it is possible to combine finite automata and continuous time variables is a way that renders their properties decidable. These are called timed automata [START_REF] Alur | A theory of timed automata[END_REF] and methods for model checking their properties are based on efficient ways for solving systems of linear inequalities. Of course, there are standard methods such as the simplex algorithm for analyzing systems of linear inequalities, but timed automata lead to problems that are both simpler and more difficult than those considered in classical linear programming: they are simpler because the inequalities are of restricted forms, and they are more difficult because different (discrete) states may have different behavior, thereby requiring much case analysis. Model checkers for timed automata, such as Uppaal [START_REF] Larsen | UPPAAL in a nutshell[END_REF] and Kronos [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF] use special representations and data structures that are optimized to the particular character of the problems generated by timed automata. There are several cases of successful application of model checking for real-time systems using timed automata, for example [START_REF] Havelund | Formal modelling and analysis of an audio/video protocol: An industrial case study using uppaal[END_REF]. However, there are few examples where real-time behavior is combined with fault tolerance. For example, a real-time startup protocol is verified in [START_REF] Pettersson | Formal verification of a TDMA protocol start-up mechanism[END_REF], but the analysis excludes the complex fault scenarios considered in the discrete-time analysis of [START_REF] Steiner | Model checking a fault-tolerant startup algorithm: From design exploration to exhaustive fault simulation[END_REF]. We conjecture that the timed automata approach is unable to handle the massive case analysis required by the large number of different fault scenarios; conversely, the treatment using discrete time can handle the case analysis, but the treatment of time is less realistic. We would like to be able to handle both dimensions-continuous time and faultssimultaneously.

Infinite Bounded Model Checking and Real-Time Systems

A bounded model checker for finite state systems works by translating the system description and property specification into a propositional SAT problem. The propositional translation encompasses both the decision and control structure of the system description (i.e., the case analysis that needs to be performed) and the operations performed on its state variables. For example, to perform the operation x + y, the translator will generate the propositional formulas that describe a binary ripple-carry adder (in effect, the translator compiles the system description into a boolean circuit). Suppose, instead, that we kept + as a mathematical operation in some decidable theory (e.g., linear arithmetic) and somehow made the SAT solver work in combination with a decision procedure for the mathematical theory. There would then be no need to restrict the state variables x and y to finite integer ranges (i.e., fixed-width bitvectors): they could instead range over the reals. The combination just hypothesized of a SAT solver with decision procedures is known as an SMT (Satisfiability Modulo Theories) solver, and the construction of such solvers is a very active area of research.

There is an annual competition for SMT solvers [START_REF] Barrett | SMT-COMP: Satisfiability modulo theories competition[END_REF] and their performance is already impressive and is improving all the time. A bounded model checker that generates formulas for an SMT solver is called an infinite bounded model checker (i.e., a bounded model checker for infinite-state systems) [START_REF] De Moura | Lazy theorem proving for bounded model checking over infinite domains[END_REF]; just like an ordinary bounded model checker, it can be used for refutation and, via k-induction, for verification [START_REF] De Moura | Bounded model checking and induction: From refutation to verification[END_REF]. The SAL tool suite provides an infinite bounded model checker that is capable of k-induction.

If we could pose analysis of real-time systems as infinite bounded model checking problems, we might be able to solve some challenging problems: the SAT solver would take care of the case analysis while the decision procedures handle the properties of continuous time. A suitable modeling approach is provided by the timeout automata of Dutertre and Sorea mentioned earlier. They present some simple real-time systems and show how these can be represented using timeout automata and analyzed using the infinite bounded model checker of SAL [START_REF] Dutertre | Timed systems in SAL[END_REF]. The analysis is not so fully automated as in timed automata: the user must generally pose and verify a series of lemmas that are combined to verify the property of interest, and that property must be formulated in a way that is appropriate for k-induction. However, the development of suitable lemmas and formulations is highly systematic (using disjunctive invariants [START_REF] Rushby | Verification diagrams revisited: Disjunctive invariants for easy verification[END_REF]), and is assisted by the counterexamples produced for inadequate formu-lations. The method yields very good performance; for example, it can verify Fischer's real-time mutual exclusion protocol (a simple benchmark in this area) with more than 50 processes, whereas most tools for timed automata cannot get into double digits. This approach has been applied and extended by others. Pike [START_REF] Pike | Real-time system verification by kinduction[END_REF] shows how the complexity of the verification problem can be reduced by using synchronous timeout automata, and by making the clock value implicit. With Johnson, he uses this method to verify a reintegration protocol [START_REF] Pike | The formal verification of a reintegration protocol[END_REF]. The decision procedures of an SMT solver allow uninterpreted constants, thus protocols can be verified with respect to parameterized quantities: instead of fixed delays such as 2 and 5 seconds, we can verify a protocol with respect to delays of Tmin and Tmax and some suitable relation between these (e.g., 2 × Tmin < Tmax). Pike and Brown use this capability to verify parameterized versions of the Biphase Mark and 8N1 decoders [START_REF] Pike | Easy parameterized verification of biphase mark and 8N1 decoders. In Tools and Algorithms for the Construction and Analysis of Systems[END_REF]. Timeout automata must be extended when components interact through the exchange of messages or by synchronizing on actions, as well as by the passage of time. Dutertre and Sorea refer to the extension as calendar automata, after the event calendars that are used in discrete event simulation systems. Using this approach, they are able to verify real-time properties of a simplified, but still fault-tolerant version of the TTA startup protocol [START_REF] Dutertre | Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata[END_REF].

Prospects

I am very optimistic about the prospects for analysis of embedded real-time systems using timeout and calendar automata, SMT solvers, and k-induction. SMT solvers are a general-purpose technology that already delivers high performance and is undergoing rapid development. The SAT solving component of an SMT solver is able to cope with large amounts of case analysis; thus fault tolerance and other sources of "case explosion" can be handled satisfactorily. Their decision procedures for linear arithmetic allow SMT solvers to handle continuous time, and other numerical quantities. Additional decision procedures (e.g., for queues) will allow automated verification for other kinds of infinite state systems. I look forward to the transfer of this technology from research laboratories into industrial practice in the near future.

Acknowledgments

The techniques and tools outlined here are the work of my colleagues Leonardo de Moura, Bruno Dutertre, Harald Rueß, Maria Sorea, and Natarajan Shankar.


Jean Souyris
email: jean.souyris@airbus.com

Towards the Product Based Assurance

Keywords: Avionics Programs, Abstract Interpretation, Dependability, Proof, RTE, Estimation of Stack Usage, WCET (worst-case execution time) Prediction

Introduction

The current state-of-the-practice of software assurance (that is ultimately confidence in correct execution behaviours) is based on the quality of development processes. Within this indirect assurance framework, verification is twofold: tests and intellectual -in the sense of non tool-based -analyses. Due to the rapid evolution of basic technologies and to the ever-increasing software implemented functions, the current state-of-the-art is foreseen to hardly scale up for engineering future avionics systems. A new approach, the Product Based Assurance, comes from the recent availability of Abstract Interpretation [START_REF] Cousot | Abstract Interpretation Frameworks[END_REF] based static analysers which make it possible to verify that program properties hold, exhaustively.

From the Process Based Assurance

In the Process Based Assurance, the confidence in the program being developed is based on the compliance of the development process with a certain state-of-the-art. DO178B is such a state-of-the-art reference for avionics programs. The rules it contains make the developers define a process which allows them -if respected -to claim that the required level of confidence in the behaviours of the program is reached. One should notice that, for a given program, the required effort for reaching the correct level of confidence varies according to the criticality of the avionics function implemented by this program. All activities of the development process are covered by DO178B, i.e., the "constructive" phases like specification, design and coding together with their relevant standards (defined by the developers) which define the rules to be followed by the specifiers, designers or coders; the verification activities like tests, intellectual analyses; the configuration management of the products of all the phases of the development; the management of the project; finally, the management of the quality. One can see that the confidence in the correct behaviour of the program execution is not only based on tests but on the full respect of a set of rules relative to all aspects of the development of an avionics program, that is the process.

A verification based on tests (by execution)

In this context a lot a efforts have been dedicated to the "descending" part of the development cycle, i.e., specification, design and coding, during the last decade whereas, in the same time, the verification techniques remained almost unchanged, at least in their principles. What are the limits of testing ? Firstly, let us separate all possible unexpected behaviours of a program into two groups: on one hand those leading to the non-respect of functional specifications without impact on the dependability of the system and, on the other hand, the ones invalidating dependability properties. For the functional aspects of the specification, testing has only the disadvantage of its limited coverage. Functional testing make it possible to select test cases whose execution give the developer a good idea of the quality of the implementation. With respect to the dependability properties, in the Process Based Assurance, the intrinsic limit of tests (limited coverage of the set of all possible executions) forces the developers to explicitly take into account as many as possible dependability properties at specification time, by adding software mechanisms which are in charge of detecting when a dependability property is violated. Indeed, when a dependability property is so "transformed" into a specification element (only if it is a safety property), it then can be handled within the Process Based Assurance framework. This enables the developers to test the above mentioned safety mechanisms. In absence of such safety oriented detection mechanisms and when testing is the only verification technique, it is not possible to prove that no undesired behaviour of the program will lead to the non-respect of a safety property. On the contrary, testing such safety mechanisms, when present, can give a good confidence in their reliability and then, if some pathological cases are not identified at test time, they will be trapped during real executions of the program. However, this approach is not fully satisfactory for two basic reasons: firstly, if a property cannot be converted into a specified monitoring mechanism or if the property is simply not considered at specification time (specifying is a difficult art…) then its verification is basically impossible; secondly, if the mechanism has been specified and coded, the potential existence of cases not covered by the tests, in which the mechanism will force the program to enter a failure mode thus limiting at least the availability of the system, cannot be excluded.

Introduction of the Product Based Assurance

The concept of Product Based Assurance is motivated by the emergence of Proof Capable Abstract Interpretation based tools which make it possible to overtake the limitation of testing, for the set of properties they deal with. The purpose is not to remove all the existing practices, but to improve them thanks to the exhaustivity of automatic static analyses. With respect to the two classes of properties introduced above, i.e., functional and dependability properties, Product Based Assurance is a lot more challenging for covering all the functional properties of a program rather than dealing with the dependability ones; and surely less urgent, for the reasons explained above. Then, in the rest of this paper, we will focus on Product Based Assurance enabled by static analysis of dependability properties.

A first set of static analysers for some dependability properties. For getting started with the Product Based Assurance, a first set of tools have been chosen; they all prove the following specificationindependent properties: resource consumption properties like stack maximum usage or Worst Case Execution Time and the absence of Run Time Errors, e.g., numerical overflows, access beyond the bounds of arrays, bad protection of shared variables, etc. Examples of such tools can be found in [START_REF] Thesing | An Abstract Interpretation-Based Timing Validation of hard Real-Time Avionics[END_REF], [START_REF] Blanchet | A Static Analyzer for Large Safety-Critical Software[END_REF].

Within the Process Based Assurance framework, these specification-independent properties are typically handled as described in section 2. Indeed, most of them lead to specify safety mechanisms which allow the detection of situations in which the properties are violated, at run-time. Nevertheless, for this set of properties, i.e., stack usage, WCET and RTE, the run-time detection of violations of these properties is not as safe as it might appear because they are often so bad for the availability that the problem becomes a safety one very quickly. Furthermore, system redundancies might be abused by such violations, which tend to be common failure modes quite easily. In this context, static analysis, with its ability to take into account all possible executions for proving that a given property holds, makes it possible to claim with more assurance that a program will never execute in less than the computed WCET, that this same program will never use more than the computed maximum stack usage and that it will not produce any RTE.

An industrial interest. The first interest of using these static analysers is mainly industrial. Indeed, at least for the first applications to real avionics programs, the safety mechanisms which act at run-time will not be removed from the code. The benefit will be an earlier detection of bugs like RTE or source of tricky bugs like stack or CPU overflows. However, one may think that, thanks to static analysis, the confidence in the program will be higher than the one obtained by only testing, specially when you consider the everincreasing size and complexity of the avionics software.

A method for each tool. A frequent misunderstanding of the usage of automatic static analysers is that their users simply "press a button". It is far form the reality. Firstly, before deciding to use such a tool on its program, the user must be aware of all the hypotheses the analyser relies on. Most of these hypotheses belong to the so-called Concrete Semantics [START_REF] Cousot | Abstract Interpretation Frameworks[END_REF]. For instance, in the case of a RTE analyser working at source code level, this semantics comprises, or takes into account, the semantics of the programming language, its particular implementation by the compiler, e.g., compiler-dependent aspects of the ANSI-C standard and, finally, some particular user requirements relative to the interpretation of some program behaviours. Secondly, before actually running a static analyser, or after a first very coarse analysis, the user must usually set some parameters, or provide the tool with additional information for fine tuning the analysis. Finally, the user has to exploit the results. Because most static analysers allow the user to start with coarse analysis and to progressively get more precise results by providing the tool with additional information, several runs, with their relevant preparation and analysis of intermediate results, are necessary for a particular type of analysis. As usual in the Process Based Assurance, in the scope of which we want to stay at least the beginning, the above activities must be well defined by methods, i.e., one per static analyser.

Conclusion

Towards a new overall proof-oriented development process. A new development process will "naturally" appear as a merge of both Process Based assurance and Product Based Assurance as the confidence in the existing and future Abstract Interpretation based static analysers will grow. Indeed, the sharing of the program verification between tests and static analysis will evolve to more proof and less test along with the conviction that taking into account all possible executions by means of abstraction is at least as important as executing a few of them on the real hardware. Moreover, an optimal complementarity between tests on the real target and static analyses will progressively be found, in order to keep the advantages of both techniques in a cost-effective way. Beyond this optimisation of the verification practices, one can imagine to relax some specification and design constraints, like removing some of the monitoring mechanisms.

In order to achieve this mutation, a new generation of Abstract Interpretation based static analysers must arise, i.e., tools aiming at the automatic proof of specification-dependent dependability properties specified by the user [START_REF] Cousot | Abstract Interpretation Based Program Testing[END_REF].

-22 -23 January 2004


Didier Blondin
email: didier.blondin@axlog.fr

Would certification become mandatory in automotive engineering

In-vehicle embedded electronic is the driving force of Automotive engineering innovation. Multiplexed networks are a step in the rationalisation's phase of functions and ecu, and we could already measure the difficult and painful integration and testing process of those sub-systems and their associated software. A new area is coming up with announced deployment of X-by-wire technologies which are going to remove a significant number of mechanical parts. Thus, some vital functions are going to be fully managed by ecu, software and electrical secured network such as TTP or FlexRay. With these new technologies, automotive market is now entering the world of safety critical embedded applications, joining there avionics and railways applications .And those transportation systems are subject to a highly regulated certification process managed by independent authority. However, the automotive industry used to be assessed by independent authority such as UTAC and EuroNCAP, whom are known for their integrity to deliver assessment of vehicle performances. If their judgment could impact the vehicle's fame, and brands opportunely use it in their advertisement campaign, it is in any case a certificate to authorize the vehicle release. While successful process through DO178B for avionics and EN 50128 for railways applications are mandatory prior to the release. Behind the stamp, certification is mainly a process, deployed by the supplier with regards to OEM and to the authority bodies (the Designated Engineering Representatives). In fact, these supervisors are checking if objectives defined over the process are achieved in terms of planning development, requirements, design, coding, testing and verification, configuration management and quality assurance. Besides traceability of the software components, a very important focus is put in place on the testing phase and coverage analysis. The testing phase is stringent, using advanced code coverage techniques such as Multiple Condition/Decision Coverage. Dependability is a key aspect for OEMs for a while, nevertheless most of the functional safety policy are based on FMEA (failure mode and effect analysis) and default trees and other math methods to check failures. Those methods are not reaching the expecting level for safety critical applications. Moreover, these investigations are managed internally by suppliers or OEMs. The critical level reached by steer-bywire or brake-by-wire is a new challenge also for OEMs with regards to liability aspect. This could be the main argument for an independent authority assessment and corresponding certification, superseding the cost argument, which is always important in the automotive market. Recent rallying of TÜV houses to the FlexRay consortium is an interesting sign.

Increasing demand for improvements in vehicle safety, performances, energy economy and low emissions has led to a great complexity in vehicle electronics. X-by-wire systems deployment will push automotive industry in the area of safety critical systems. Such as other industry, automotive community will have to set up new standards for systems validation. Within those systems, the role of software is crucial and we are going to explore in this paper the different solutions for OEMs and suppliers to insure quality of their systems and vehicles and safety of their customers. Compared to industries also using such electronic systems , a certification process would become mandatory .This analysis will cover potential solutions for the process and technologies skills but also the economical impact as well as the impact on business relationship between players of the industry.

The software crisis

Increase of embedded electronics in vehicle bring new constraints known of all of us. Impacts are double. From one side, in the development process where suppliers have to face the raise of software size, i.e. engine control where the size of ROM is doubling every two years. Moreover, OEMs have to deal with validation of the networked car and the multiplexed architecture with ecu provided by several suppliers. This distributed architecture over the vehicle and the interaction between functions set up a real challenge the test and validation of the overall vehicle network.. From the other side, OEMs are now measuring the consequences of the lack of efficient validation process and skills with recalls due to software failures which have very bad impact on the brand image. Two new trends strengthened those difficulties. The first one is the integration of software functions provided by different suppliers for a single ecu. It seems that we have reached the point where the number of ecu is stabilized when the number of functions is still increasing, with more and more interactions, ie. avoidance collision system with ESP, ABS and engine control. When a segment model owned twenty five ecus for two hundred functions, the next model will keep those twenty five ecu but to manage six hundred functions. The other trend is the up-coming x-bywire technology which will supersede soon classical electro-mechanism and hydraulic system such as brake and steer. Those new fault tolerant protocols, namely TTP/C and FlexRay, will bring a new area in automotive electronics, doesn't matter which one will become The standard , even if nowadays, FlexRay seems to have the lion's share in its corner [START_REF] Hansen | The Hansen Report[END_REF]. Level of redondancy and protocol validation are points not yet clear that needs more investigation but one conclusion raised: with by-wire technologies, the car is entering the world of safety critical systems.

Certification standards

Such evolutions occurred some years ago in industry such as the avionic industry and the railways industry. More recently, the electrical industry also engaged with same approaches. Dependability methods were crucial to ensure safety of those systems. And it is now mandatory to certify safety critical systems in those areas. Certification standards are now well established, applied and mastered into those industries. Let's remind that aircraft manufacturer deal with RTCA/DO-178B (Eurocae-ED12B) which provides stringent guidelines for the production of software for airborne systems and equipment certification [START_REF] Rtca | Software considerations in Airborne systems and equipment certification[END_REF]. Railways industry deals with EN 50128 "Railway Applications: Software for Railway Control and Protection Systems". A more generic standard applied to electrical and electronic equipment with IEC 61508, safety of electrical/electronic/ programmable electronic (E/E/PE) safety-related systems. Those standards specify levels of safety performance for a safety function. The RCTA/DO-178B defined five levels from E to A, the level A standing for catastrophic scenario. IEC 61508 defines 4 levels called software integrity levels (SIL) from 1 to 4 [START_REF]IEC, International standard; Functional safety of electrical/Electronic/Programmable Electronic Safety-Related Systems -Part3: software reqs[END_REF].

Let's see in the figure 1 below what could be the categorization of systems into a car compared to an aircraft. Note here that we have applied IEC 61508 to this scenario. Two main reasons: RTCA/DO-178B is not applicable to automotive according to all of you who have looked at this consideration; IEC 61508 appears now in some OEMs request for quotation, although it mentioned IEC 61508 compliant rules rather then certification.

A mature process

At this point, we need to dig behind the wording of certification. In fact the standards are not prescriptive.

Guidelines are provided to reach objectives which should be fulfilled to get the certification stamp. These guidelines are mainly oriented assessments and processes through hazard analysis, requirement traceability, design, coding, review, test, validation, configuration management, quality assurance …A generic overview is represented in figure 2.

Depending of the certification level expected, the verification and validation phase is gradually stringent until full coverage analysis through Multiple Condition/Decision Coverage analysis. Generally speaking, a software hazard and operability analysis (HAZOP) and failure mode and effect analysis (FMEA) are integrated in the process. Is the automotive industry far from this level of process for their software development? Absolutely not! Let's have a look on current methods and use. Due to market trends, mainly cost pressure and time to market, OEMs and suppliers have deployed formal methods to reach an efficient teamwork. Requirements management tools and executable specification environment are in place for years to ensure early validation of design and requirement traceability through the overall lifecycle. Assurance quality plans are deployed for a while and SPICE-ISO/IEC 15504 or CMMI appear now as the de facto-standard to still be alive in the business. Specific automotive guidelines are also in use such as MISRA [START_REF] Misra ; Misra | Development guidelines for vehicle based software[END_REF]. Dependability is crucial for OEM for years and lots of efforts are put in place currently to improve software aspect of software, especially with regards to x-bywire technologies [START_REF] Gilbert | Processus et méthodes de sûreté de fonctionnement applicable au by-wire[END_REF]. Preliminary risk analysis (PRA) and FMEA are mastered by systems architecture teams. On the other hand, suppliers and OEMs have a huge expertise in unit test and integration test phases.

Fig. 2: V cycle and certification process

In vehicle testing approach are now superseded by simulation and if the testing process still need to be improved, the automotive industry gets all the knowledge and background to formalize a certification process.

Cost as the biggest threat

So, why is the industry so reluctant to the certification concept? One response is the lifecycle model of ecu. When a model year is released, lots of software updates are released for a single ecu . For a engine control unit, new software versions occurs every 4 to 6 months. This approach is not compliant with constraints of certification. From an other hand, today, OEMs have the full responsibility to release a car, without the need to carry out assessment programs on the systems. Launch of new models are planned months ahead, with well defined plant planning and marketing and advertising campaign, and it is the sole decision of the carmaker to decide this date. OEMs may be upset to lose this autonomy. Finally, and probably the main reason, is the cost aspect of certification. Certification process and cost of an Airbus which cost fifty millions euros and will be produced for two hundred units is mandatory. What about applying similar rules for a car which is twenty thousand euros for two hundred fifty thousand units? The ratio is not so far. But nowadays, all OEMs are engaged in cost killing plan and each cents that could be saved is saved.

Extensive test coverage report

Another aspect regarding certification is the certification authority. Integrity and worldwide recognition are mandatory to gain the full acceptance of the industry, whatever it is. Figure 3 illustrates the certification process in the aerospace industry in France. Is this model applicable to automotive? In the role of EASA, an international organisation issued of the automotive industry should take place. Such organisation already exists for other purpose in the industry i.e. EuroNCAP. Automakers feel so concerned about results that they are using it for their advertising campaign. Obviously, it's too late now for the industry to create from scratch a automotive standard for certification. It took twenty years to the aircraft industry to reach the point of skills where it is today, in terms of processes as well as infrastructure. The automotive community needs to speed up to accept this challenge. The solution currently planed is to adopt an existing standard.

Business relationship

One main factor could speed up the process, the liability of OEMs. Once by-wire technologies will be deployed, software failures are forbidden otherwise in case of severe injury, lawyers may become the worst enemies of carmakers, with consequences on brand image and sales of sensational trials. The business relationship between suppliers and OEMs will evolve as well. Today, when ecu failed it is Tier1's problem, and insurance are usually part of the procurement. With interaction between function and distributed architecture, OEMs are going to take more responsibilities, as they will be responsible for the all architecture behaviour. They will have to become more stringent as well with their suppliers. The good news for suppliers: this change will emphasis the added value of software and there will be a turn in the story where software will get its own value.

Conclusion

In this paper, we've describe the certification standards in use in some industry. We have analysed the trends of the automotive industry and deducted that a certification process will be mandatory in a close future. Some investigations have been done to list questions the automotive community should answer shortly. We've concluded that there is no technical barrier for the industry to dig into a certification process. Only political and business issues have to be solved in order to speed up a process which seems irrevocable for us but still to be defined.

Fig. 3 :

 3 Fig.3: Aircraft certification process

-22 -23 January 2004