Mathieu Clabaut
email: mathieu.clabaut@systerel.fr

Christophe Metayer
email: christophe.metayer@systerel.fr

Éric Morand
email: eric.morand@cnes.fr

Formal Data Validation Formal Techniques Applied to Verification of Data Properties

Keywords: Dependability, safety, security, quality of service Domain. Verification and validation MmdlSMemoryArea tMmdlMemoryMappingTable[14] = { {0x34000, 0x17000, 1, PARTITION_CODE, {0x4B000, 0x800, 1, CONFIG_TABLE, FLASH}, {0x4B800, 0x200, 1, CUSTOM_TABLE, FLASH}, {0x4C000, 0xC000, 2, PARTITION_CODE, FLASH}, {0x4B000, 0x800, 2, CONFIG_TABLE, FLASH}, {0x5C000, 0x10000, 3, PARTITION_CODE, FLASH}, {0x40070000, 0x1C0000, 1, PARTITION_CODE, RAM}, {0x40230000, 0x20000, 1, CONFIG_TABLE, RAM}, {0x40250000, 0x20000, {0x40270000, 0xC000, 2, PARTITION_CODE, RAM}, {0x4027C000, 0x4000, 2, CONFIG_TABLE, RAM}, {0x40280000, 0x10000

Nowadays lot of critical systems used in aeronautic, aerospace, automotive and railway domains are designed to be highly configurable. In such systems, the data configuration validity is of tremendous importance. The railway domain does already apply some formal techniques to validate configuration data. This study, funded by the CNES, demonstrates the suitability of such methods for validation of flight software configuration data. Topic.

Context and Goals

Context

Complex systems in the aerospace domains are required to be more and more adaptable and reusable, and hence tend to be based on generic software configured by means of data parameters.

Validation of such generic software follows two approaches: either the generic software and its configuration are validated together for the targeted deployment or the software and its configuration are validated separately if possible or else in a two stage validation where data are validated before the configured software.

Our experience about data validation is that:

-it is often done by procedural means, an ad-hoc software being developed to achieve the verification. -properties on configuration data, whenever identified are often considered as second class citizens.

It has been shown that such verification tools are difficult to maintain when the properties evolve.

The algorithmic implementation of the properties not only is being written by someone who is not acquainted to the domain they are related to (namely a software designer) but also has the unwanted side effect of obfuscating them. An external assessor thus has the greatest difficulties to ensure that desired properties are those verified by the tool.

Based on some successful experiments on applying formal techniques to validation of configuration data for the railway domain, we were willing to apply them to space flight software, and especially to basic software (BSW) configurations.

Goals and Planning

Expected benefits of the study are:

-clear property identification and formalisation; -automatic property verification on binary code; -demonstration of feasibility, usability and improvements over previous verifications.

Two main tasks were devised when planning the study:

1. harvest the known and possibly unknown properties of BSW data configuration and formalize them within a rather simple mathematical language (first order predicate, set theory). 2. write some tools to automatically extract data from binary code and verify the properties on these data.

Data Validation for Railways

A bit of history Historically, interlocking systems were designed by means of physical levers and cotter pins and were carefully designed to avoid enabling conflicting routes. A century ago, all-electric interlocking made up of electrical relays began to be designed. However each interlocking system is still specifically designed to avoid enabling conflicting routes on a well defined area. Since the late 1980s, most interlocking engines are fully implemented in software. As the cost for developing such a SIL4 system is quite high, manufacturers are faced with the problem of designing a generic enough interlocking engine 4 which would accommodate most of the existing ground configurations by means of configuration.

Such a (big) configuration data set is then a full contributor to the global safety level, and as such must be validated thoroughly.

Data Validation, the old way Validating huge data configuration set against complex properties is quite a daunting task, and needs automation. For this purpose, manufacturers began to develop software specifically designed to verify the configuration data set against some expected properties.

Those software were written in C or C++ and the expected properties as well as the format of the configuration data were hard-coded in their internals. The following consequences soon arose: validation cost: the whole data validation software has to be validated, not only the properties, actors involved: the domain experts have no means to check that the properties verified by the software are the expected ones and conversely, the software engineers aren't domain specialists. This sometime leads to inconsistency between what was checked and what ought to be checked, evolution cost: modification of a property requires to modify the software and to revalidate it, product line: developing a similar subsystem requires to develop again most of the data validation software

The whole process was cumbersome, error prone and expensive.

Data Validation, the new way Some years ago, RATP began to rethink the way configuration data were validated and a tool was developed upon the opensource platform Rodin [START_REF]Rodin -rigorous open development environment for complex systems[END_REF] to validate those data against safety properties which would be formally specified.

The chosen formal language is a subset of the B language [START_REF] Morand | The B-book: assigning programs to meanings[END_REF] which can simply be seen as a first order predicate logic over set theory using a notation which shares a lot with standard mathematical notation (∃, ∀, ∨, ∧, ∪,…) which was perfected for several centuries and is well understood by most engineers and which, due to its formal nature, is also understandable by computers (see figure 1).

Fig. 1. Mathematical formal language as the best compromise between human and computer

The foundations were then laid for the building of a modular software platform allowing verification of formal properties over a wide range of data.

The following sections will elaborate a bit on the case study perimeter, properties and data considered, tools developed and used and the results obtained.

Case Study

We describe hereafter the chosen case study which consists in the configuration of the GPMU BSW.

Satellite GPMU

The Generic Payload Management Unit (GPMU) is the part of the satellite (hardware and software) in charge of hosting the payload software which will provide the set of functions enabling the satellite to fulfill its mission (by contrast with the platform part, which provides basic services like energy sources and positioning system).

The GPMU architecture is described in figure 2, and is based on the XtratuM hypervisor [3]. GPMU is composed of a resident software (not shown) which loads and launches the hypervisor which offers a spatial and temporal partitioned environment for running different OS. The hypervisor virtualises services offered by the physical platform in order to make them available to the various hosted OS.

Onboard processor

The Basic Software (BSW) is a subsystem which isolates the payload management functions from the mission specific functions. It is composed of several distinct partitions which offer functions related to:

-mode management, -inter-partition I/O management, -non volatile memory management, -hardware and instrument events management, …

We will focus our analysis on the MMDL BSW partition which offers high level services to manage application partitions (memory mapping, partition monitoring,…), and on the IOSERVER BSW partition which offers services to manage inter-partition and device communications. Those services are provided by mean of the PMU protocol and all partitions, whether they belong to the Basic Software or not, will use the PMU protocol for inter-partitions communications with the Basic Software. Others communications, for instance between two non BSW partitions, can be opaque and so may not use the PMU protocol.

Partitions outside BSW offer mission specific functionalities.

Partitions Configuration

While each development team is responsible for its partition the person responsible for integration shall produce the hypervisor configuration table by fulfilling the following tasks:

-collect characteristics and constraints for each partition, -configure the hypervisor with each partition (memory mapping, …), -configure the I/O management for each partition, -configure the inter-partition I/O ports, -configure the I/O scheduler, -configure the partition scheduler, -test and validate the global GPMU behaviour.

Our study will concentrate on the production of the BSW MMDL and IOSERVER configuration tables, whose complexity comes from the number of dependencies between the a priori chosen partition scheme, and the a posteriori constraints (I/O, memory mapping, …).

Properties

What does Data Validation mean?

And what are data anyway? The set of considered data are constants that contribute to the configuration of a system. They may be -physical constants, -parametric constants which are used to define a command law, -mission specific constants (which may be uploaded), -parametric constants specific to the design choices, -validation and test data, -constant produced while defining the configuration data (authors, creation date, version, integrity,…)

Properties link different types of data. They exist independently from the system being active or not and define invariants over the system.

Validating data is the act of verifying that the configuration data verify the properties (most often, safety ones) identified.

Of course, validating data is necessary but not sufficient to ensure the correctness of the system behavior.

Property Identification

The first part of the job is to informally identify which properties shall be verified by the configuration data. The following available documentation was taken into account:

-XtratuM hypervisor User Manual, -XtratuM hypervisor Reference Manual, -BSW User Manual, -A first identification of some coherence rules.

We began to dig out and express in natural language some required properties, which may be categorized as follow:

A properties relative to the domain of scalar constants.

One shall mainly verify that a scalar parameter is defined within its bounds or that its extremum values are compatible with the hypervisor configuration, B equality constraints.

For example, verify that the size of a structure is equal to the value of another parameter, C parameter typing.

Verify that all data loaded in a structure respect the structure type, D coherence between data.

For example, check that some memory spaces are disjoints for a given partition, or that the communication port characteristics for interconnected ports are compatibles, or check unicity within specified structures…

The configuration scheme chosen for the BSW which compiles configuration files written with the help of the C language, ensures that properties of type C are verified. Those properties won't then be addressed in the following.

An example of simple property of type A, extracted from the available documentation is shown hereafter in figures 3 and 4. The actual configuration as found in the .c file is shown in figure 5. A more complex property of type C is inferred from our understanding of the system and from actual data configuration as shown in figure 6. It says that memory mapping defined for a given partition id are disjoints.

Fig. 6. Memory mapping table

Some properties may also come from standard conformance or from other design constraints, like saying that existing hardware should be used when possible. One example of such a property is: UART components have normalized speeds.

However it is often very difficult to exhaustively identify properties that should hold upon configuration data once system design is over.

This last statement promotes an early integration of property management in a system development cycle.

Property Formalisation

Once the properties are identified, we define a formal model which describes the data constants and properties as axioms over the constants. The use of event-B [START_REF]Event-b -a formal method for system-level modelling and analysis[END_REF] allows us to decompose the model as shown hereafter.

/ / Range d e f i n i t i o n f o r memory o p e r a t i o n p o r t s i z e @axm1 : MIN_MEMORY_OPERATION_PORT_SIZE ∈ ℕ @axm2 : MAX_MEMORY_OPERATION_PORT_SIZE ∈ ℕ / / I n and Out p o r t s i z e d e f i n i t i o n

@axm1 : sMmdlMemOpInPortSize ∈ ℕ @axm2 : sMmdlMemOpOutPortSize ∈ ℕ / / A c t u a l p r o p e r t y over t h e p o r t s i z e being i n i t s range @axm11: sMmdlMemOpInPortSize ∈ MIN_MEMORY_OPERATION_PORT_SIZE ‥ MAX_MEMORY_OPERATION_PORT_SIZE @axm12: sMmdlMemOpOutPortSize ∈ MIN_MEMORY_OPERATION_PORT_SIZE ‥ MAX_MEMORY_OPERATION_PORT_SIZE

The constraint about disjoint memory mapping being defined for a given partition id may be formalized as follow 5 :

/ / MmdlSMemoryArea f i e l d s d e f i n i t i o n @axm4 : StartAddress ∈ 1 ‥ MemoryMappingTableSize → ℕ @axm5 : Length ∈ 1 ‥ MemoryMappingTableSize → ℕ @axm6 : PartitionID ∈ 1 ‥ MemoryMappingTableSize → ℕ

/ / p r o p e r t y f o r d i s j o i n t memory mapping

@axm9 : ∀ i,j • i ∈ dom(StartAddress) ∧ j ∈ dom(StartAddress) ∧ i ∈ dom(Length) ∧ j ∈ dom(Length) ∧ i ∈ dom(PartitionID) ∧ j ∈ dom(PartitionID) ∧ i ≠ j ∧ PartitionID(i) = PartitionID(j) ⇒ StartAddress(i) ‥ StartAddress(i)+Length(i) -1 ∩ StartAddress(j) ‥ StartAddress(j)+Length(j) -1 = ∅
Where dom(f) denotes the domain of function f. The constraint about UART speeds may be formalized as follow: Where ran(f) denotes the range of function f.

/ / Constant d e f i n i t i o n and t y p i n g

Beyond the possibility of data validation, having defined such a formal model for properties allows:

-a formal expression not only for the properties but also for the associated data structures, -a proof of well-definedness of properties and a verification of their types, -the use of a simple and common enough formalism, shared by the different actors, -a separate validation for the proof mechanism and for the data (the proof mechanism shall be validated only once), 5 where A → B is the set of total function from A to B.

Data Extraction

General Case

From our previous experiences in validating data for the railway domain, it appears that data come from various sources and be encoded into various formats (DBMS, XML files, structured text files, flat text files, ADA or C source code). It is not conceivable to devise a piece of software which would be able to manage such a variety of sources and format. Thus the software that verifies formal properties on data (lets call it data prover) was designed to be data source agnostic but expandable by means of plug-ins to be able to get data from sources that were not envisioned at the time of initial design. With safety in mind, we want to check the data as late as possible in the configuration process in order to prevent as much as possible data corruption to happen after the verification being done.

The very last place where most of the configuration data may still be understandable for an external piece of software, is in the ELF binary object produced by compiling the configuration .c source files. However data types may not be inferred from the binary ELF file and shall be provided to the extractor by another channel.

With the objective to be as efficient as possible, we have chosen to develop an extractor with buit-in data type information. It is a bit less convenient as the extractor shall be compiled again when the data types change, but it allows us to exhibit some results in a limited time and budget.

The overall process is shown in figure 8 hereafter.

Tools

A short overview of the tools developed or used during this study is given is the following section. The tools are:

-a data extraction tool for harvesting configuration data from binary objects, -a formal development platform for checking that properties were well typed and well defined (i.e. meaningful),

-the core of the data prover tool, which was improved and used over the properties and associated configuration data.

Data extraction from Binary Objects

A tool was coded in C, to extract the data from the binary objects based on their ELF format, which by mean of relocation tables allows us to find values of constants defined as static const in the .c piece of code which defines the configuration data.

In order to simplify the whole development, the expected data types, which can not be inferred from the data provided by the ELF format, are hard-coded in the extractor tool which produces a simple XML file. This XML file will then be used by a small data prover plugin to translate the XML representation into the targeted internal data constant representation.

An extract of such an XML file obtained from actual analysis of binary configuration objects is shown in figure 9.

<?xml version="1.0" encoding="ISO-8859-1"?> <constants> <scalar name="lOutDataRxQueuingPortsNumber" type="UInt32 " value="3"/> <scalar name="lInDataTxQueuingPortsNumber" type="UInt32" value="3"/> <scalar name="lOutDataAckQueuingPortsNumber" type=" UInt32" value="3"/> <array name="cTableOutDataRxPortNames" type="Int8*"> <string value="QIOPFTCO"/> <string value="QIOI1TMO"/> <string value="QIOI2TMO"/> </array> <array2 name="cInDataTxConnectionTable" type="UInt8"> <row> <number value="1"/> <number value="0"/> <number value="0"/> </row> <row> <number value="0"/> <number value="1"/> <number value="0"/> </row> <row> <number value="0"/> <number value="0"/> <number value="1"/> </row> </array2> </constants> Fig. 9. Intermediate XML data description extracted from binary objects (short extract)

Static Checking of Formal Properties

We choose to use the existing Rodin [START_REF]Rodin -rigorous open development environment for complex systems[END_REF] platform as supporting tool to develop the formal model of properties. It brings the following advantages:

-easy input of mathematical formulas, -easy formula reading by mean of UTF8 characters and syntax highlighting, -use of event-B [START_REF]Event-b -a formal method for system-level modelling and analysis[END_REF] model structures to decompose the formal model, -transparent type checking of the formal model, -transparent proof obligation generation for welldefinedness, -transparent automatic proving attempt of those proof obligations, -assisted manual prover for the remaining undischarged proof obligations if any, -easy model import by the data prover. Thus, while any data verification tool developed in a low level language (say C, for example) would have allowed to check a string pointer against an integer without any hiccup, it won't even be possible to type check the corresponding property in our formal model.

This definitely leads to a data validation of better quality.

Data Validation against Formal Properties

The last tool developed within this study is the core data prover, based on existing pieces of code from the Rodin platform, which once fed with:

-the formal context defined as event-B contexts components, -the properties to be verified defined as event-B axioms in terms of constant and types defined in the associated contexts, -the data XML file produced from the binary configuration objects by the data extractor tool, will verify in turn each property (axiom) against the provided data and will produce a status similar to the one provided in figure 10. 6 Results

Achieved Work

This study allowed us to show that the validation of data based on formal property expression, which has already been used in the railway domain is also applicable to on-board basic software configuration for the space domain.

Even if the properties verified in this study are most often simple ones, our past experience has shown that such a process scales well to more complex properties upon a lot of data provided that associated data are easy enough to extract 6 .

It was also shown that a difficult task is to identify the properties to be checked. They are not always written down in available documentation. Having to formalize the properties won't help much in finding them, but it is a great mean to capitalize those properties and to integrate them in the whole development cycle.

Further work

Domain of Application

It would be interesting to extend the data verification for on-board software to complete satellite system (including the satellite platform, with its related configuration and calibration constraints).

There are also probably lots of other domains outside railways and space that may benefit of such an approach, provided people are conscious of the existence and the role of the properties that should hold upon their configuration data.

Tool Improvements Tools developed within this study may be improved in several ways:

-data extraction should not need recompilation upon data type change, -natural language expression of properties shall be integrated into the formal model or a document shall be produced mixing formal and informal expression of properties to allow validation by domain experts.

The report result should also refer to the natural language expression of properties, -a user interface should be provided to allow inspection of the data set that falsifies a property, to ease the spotting of the configuration data responsible for the property falsification.

Get More from Formal Methods We could imagine to integrate completely the verification framework within the Rodin platform, by making the property verification tool being one of the available prover. It would allow verifiers to decompose and prove very complex properties with the help of the whole tool set without restricting to symbolic evaluation.

Identifying Properties Afterward is probably one of the most difficult point raised by this study. Having the tools and methods for deploying easy data validation would probably be a good incentive for including property management since the beginning of the system development cycle.

Fig. 2 .

 2 Fig. 2. GPMU architecture

Fig. 5 .

 5 Fig. 5. Memory port size as defined in the configuration file (C language)

Fig. 8 .

 8 Fig. 8. Data extraction and verification process

OKFig. 10 .

 10 Fig. 10. Verification results (where some properties are falsified)

  Constant and property model architecture for MMDL partition Two models were defined, one for the MMDL partition which defines the properties about the memory mapping table, the partition information table and the monitored partitions table; and one for the IOSERVER partition which defines the properties about the device description table and the scheduling plan table.

		.	ranges defi-. nition context
			. extends
		. type definition
			context
	. e x t e n d s		. extends	. e x t e n d s
	. Memory Map-ping model	. Partition Info model	. Monitored Partition model
	Fig. 7.

Note that other subsystems of automatic train protection systems have the same requirements upon safe and voluminous configurations.

Glossary

BSW Basic Software ELF Executable and Linkable Format GPMU Generic Payload Management Unit interlocking system Railway system which establishes train routes by mean of points and signals. MMDL Mode Management and Data Load SIL Safety Integrity Level a relative level of riskreduction provided by a safety function. PMU Payload Management Unit 6 For example, our solution won't help for proving properties over unstructured data to be extracted from PDF documents.


Duncan Brown
email: duncan.brown.jvaec@rolls-royce.com

Hervé Delseny
email: herve.delseny@airbus.com

Kelly Hayhurst
email: kelly.j.hayhurst@nasa.gov

Virginie Wiels
email: virginie.wiels@onera.fr

Guidance for Using Formal Methods in a Certification Context

Keywords: Certification, aeronautics, formal methods

  L'archive ouverte pluridisciplinaire

Introduction

DO-178B/ED-12B, Software Considerations in Airborne Systems and Equipment Certification [1], is the current basis for software assurance in the civil aeronautical domain. Formal methods can be applied to many of the development and verification activities required for software used in this domain. When DO-178B/ED-12B was published in 1992, formal methods were briefly mentioned as a possible alternative method. Since that time, advances and practical experience have been gained in techniques and tools supporting formal methods, to the extent that many formal methods have become sufficiently mature for routine application on today's avionics products.

For the past four years, RTCA and EUROCAE have sponsored a joint special committee/working group (SC-205/WG-71) to update DO-178B/ED-12B to take into account and facilitate the appropriate use of new software engineering techniques that have emerged since 1992. The committee is updating the core document DO-178B/ED-12B, and four new documents, called technical supplements, are being developed to handle specific topics including tool qualification, object-oriented approaches, model based development, and formal methods. Subgroups have been created within the joint committee to define these technical supplements. Sub-group 6 is in charge of formal methods. This paper reports on sub-group 6 work and achievements to date towards creating a technical supplement for formal methods.

After briefly synthesizing the current content of DO-178B/ED-12B, this paper first highlights the essential characteristics of formal methods, then describes the objectives proposed for the Formal Methods Technical Supplement (FMTS). The main goal of this supplement is to define how formal methods can be used within a DO-178/ED-12 project.

DO-178B / ED-12B

Developing airborne avionics software in compliance with the DO-178B/ED-12B standard is the primary means of securing regulatory approval [2]. DO-178B/ED-12B does not prescribe a specific development process, but instead identifies important activities and design considerations throughout a development process and defines objectives for each of these. DO-178B/ED-12B distinguishes development processes from "integral" processes that are meant to ensure correctness, control, and confidence of the software life cycle processes and their outputs. The verification process is part of the integral processes along with configuration management and quality assurance. This section gives an overview of the development and verification processes, since the use of formal methods affects those processes.

Development processes

Four processes are identified as comprising the software development processes in DO-178B/ED-12B:

• The software requirements process develops High Level Requirements (HLR) from the outputs of the system process; • The software design process develops Low Level Requirements (LLR) and Software Architecture from the HLR; • The software coding process develops source code from the software architecture and the LLR; • The software integration process loads executable object code into the target hardware for hardware/software integration.

Each of these processes is a step towards the actual software product. Figure 1 presents the relationships among life cycle data items from the development processes.

System Requirements

High-Level Requirements

Source Code

Executable Object Code

Development activity

Note: Requirements include Derived Requirements

Software Architecture

Low-Level Requirements

Fig. 1. DO-178B/ED-12B development processes

Verification process

The results of the four development processes must be verified. Detailed objectives are defined for each step of the development, with some objectives defined on the output of a development process itself and some on the compliance of this output to the input of the process that produced it. Figure 2 presents the verification objectives and activities in relationship with the development artifacts. Each verification activity is depicted by a dashed arrow and the objectives which it satisfies are annotated on the arrows. For example, LLR shall be accurate and consistent, compatible with the target computer, verifiable, conform to requirements standards, and they shall ensure algorithm accuracy. On the other hand, LLR shall be compliant and traceable to HLR.

Traceability

Fig. 2. Verification objectives and activities

In addition to these verification objectives in DO-178B/ED-12B, there are also objectives defined for verification of verification; that is, how to be sure the software has been sufficiently verified.

The verification of verification objectives require that a coverage analysis be done. A functional coverage analysis is required to ensure that test cases have been developed for each requirement. A structural coverage analysis is required to ensure that the software structure has been sufficiently exercised, with different coverage criteria depending on the criticality level of the software.

Characteristics of formal methods

The proposed guidance for the FMTS begins by defining what formal methods are from the perspective of DO-178B/ED-12B: that is, a formal method is a formal analysis carried out on a formal model. This perspective is important because it permits discussion of formal methods according to the major life cycle processes called out in DO-178B/ED-12B, especially development and verification processes. Development processes are applicable to formal models, and verification processes are applicable to formal analyses.

In general, a model is an abstract representation of a given set of aspects of the software that is used for analysis, simulation and/or code generation. In a certification context, to be formal, a model must have an unambiguous, mathematically defined syntax and semantics. This makes it possible to use automated means to obtain guarantees that the model has certain specified properties.

Although there are important benefits in creating formal models of cycle artifacts, the most powerful benefits of formal methods are in the formal analysis of those models. Formal analysis can provide guarantees or proofs of software properties and compliance with requirements. Proof, or guarantee, implies that all execution cases are taken into account. For the purpose of the FMTS, an analysis method can only be regarded as formal analysis if its determination of a property is sound. Sound analysis means that the method never asserts a property to be true when it may not be true.

There are many different kinds of formal analysis, but they can typically be classified in three categories: (1) deductive methods, such as theorem proving, (2) model checking, and (3) abstract interpretation.

Deductive methods involve mathematical arguments, such as mathematical proofs, for establishing a specified property of a formal model. A correct proof of a property provides rigorous evidence of that property for the formal model. These proofs are typically constructed using an automated or interactive theorem proving system. Even with such assistance, constructing proofs can be difficult, or impossible in some cases. However, once a proof is completed, automatic checking of the correctness of that proof is usually trivial.

Model checking explores all possible behaviors of a formal model to determine whether a specified property is satisfied. In cases where the property is not satisfied, a counter-example is generated automatically illustrating where and how the property fails to hold. In some cases, a model checker may not be able to determine if the given property holds; for example, in cases where the complexity of the model exceeds the capacity of the model checker.

Abstract Interpretation is a theory for formally constructing conservative representations (i.e. enforcing soundness) of the semantics of programming languages. In practice, this method is used for constructing semantics-based analysis algorithms to determine dynamic properties of infinite-state programs. With abstract interpretation, a formal model is generated, usually within a tool that is specific to the particular property under analysis. It can be viewed as a partial execution of a computer program which determines specific effects of the program (e.g., control structure, flow of information, stack size, number of clock cycles) without actually performing all the calculations.

Development using formal methods

The development artifacts shown in Figure 1 can be specified using a formal model. This is no different, in effect, from using any other language to specify a development artifact, except that using a formal notation allows some of the verification objectives to be satisfied by the use of formal analysis. Formalizing requirements or design may increase the effort required to specify them, compared with using more conventional languages, but may result in additional errors being found and removed earlier during this process due to the additional scrutiny inherent in applying a formal notation.

It is worth noting that not all of the requirements for any given development artifact need to be defined formally when using a formal method. For those requirements which are not formally defined, DO-178/ED-12 guidance should be used.

From the perspective of meeting the DO-178B/ED-12B objectives for development, no special guidance is needed when using formal methods. If the applicant does not plan to use formal analysis in the verification, then there is no need to comply with the FMTS.

In cases where formal analysis is planned, the development activities should ensure that there is sufficient definition in the formal model to verify properties about the artifacts being analyzed. The software architecture can be analyzed independently of low level requirements. In the same way low level requirements can be analyzed independently of high level and architectural requirements. Some methods create a formal model at the source code level, embedding information flow from the design into the code, which is then checked by formal analysis. It may even be possible to apply formal methods to analyze properties of object code. In this case, object code is a formal model whose semantics are treated the same by the formal analysis as they are by the target hardware.

Verification using formal methods

With formal analysis, the correctness of life cycle data with respect to a formal model or property can generally be proved or disproved; therefore, formal analysis is able to replace the conventional methods of review, analysis, and test, as specified in DO-178B/ED-12B, for some verification objectives. The guidance proposed for the FMTS details the potential use of formal methods at each development level and gives the conditions for the use of a given formal analysis for a given verification objective.

Meeting the DO-178B/ED-12B objectives for verification of verification process results is more complicated when formal analysis is used. In cases where testing alone is used, verification of verification is accomplished by a coverage analysis to guarantee that software has been tested enough. However, test coverage metrics, such as decision coverage or modified condition/decision coverage, are not meaningful for analyzing the sufficiency of a formal analysis. For the FMTS, an alternative approach to coverage is proposed when formal analyses are used to replace some testing.

Reviews and analyses

For requirements (HLR and LLR), architecture and source code, the use of formal methods is a particular case of analysis. Thus the "only" guidance needed for formal analysis in these cases is the criteria and conditions for the use of formal methods for each development process; the objectives have not been modified. That is, formal analysis can be used to satisfy the objectives for software reviews and analysis, as shown in Figure 2, as follows: a. Compliance: If the life cycle data items that comprise the inputs and outputs of a software development process are formally modeled, then formal analysis can be used to verify compliance. Compliance can be demonstrated by showing that the output satisfies the input. Formal methods cannot show that a derived requirement is correctly defined and has a reason for existing; this must be achieved by review.

b. Accuracy: Formal notations are precise and unambiguous, and can be used to demonstrate accuracy of the representation of a life cycle data item.

c. Consistency: Life cycle data items that are formally expressed can be checked for consistency (the absence of conflicts). If a set of formal statements is found to be logically inconsistent then the inconsistencies must be addressed before any subsequent analysis is conducted.

d. Compatibility with the target computer: Formal analysis can be used to detect potential conflicts between a formal description of the target computer and the life cycle data item.

e. Verifiability: Being able to express a requirement in the formal notation defined in the software verification plan is evidence of verifiability in the same way as being able to define a test case. In some cases, formal analysis is better able to verify a requirement then testing.

For example, requirements involving "always/never" cannot in general be verified by a finite set of test cases, but may be verified by formal analysis.

f. Conformance to standards: Life cycle data items that are formally expressed must be compliant with any standards defining the formalism. Invalid results will be obtained if illformed requirements are allowed. Since formal notations have a well-defined syntax, automated syntax checkers are appropriate for verifying that the formally stated requirements are well-formed with respect to syntax. In addition, an automated checker may enforce other restrictions on the notation (e.g., complexity of notational constructs and other design constructs that would not comply with the system safety objectives). Automated checking will need to be supplemented by review for those standards not amenable to automated checking.

g. Traceability: Traceability ensures that all input requirements have been developed into lower level requirements or source code. Traceability from the inputs of a process to its outputs can be demonstrated by verifying with a formal analysis that the outputs of the process fully satisfy its inputs.

Traceability from the outputs of a process to its inputs can be demonstrated by verifying with a formal analysis that each output data item is necessary to satisfy some input data item.

h. Algorithm aspects: If life cycle data items are formally modeled, then algorithmic aspects can be checked using formal analysis.

i. Requirement formalization correctness: If a requirement has been translated to a formal notation as the basis for using a formal analysis, then review or analysis should be used to demonstrate that the formal statement is a conservative representation of the informal requirement. It is important to note that the preciseness of formal notations is only an advantage when they maintain fidelity to the intent of the informal requirement. If the semantic gap between an informal statement of the requirement and its embodiment in a formal notation is too large, then establishing that the formal statement is conservative may be difficult.

Test

Using formal analysis to meet the verification objectives for executable object code is the biggest challenge for providing guidance because test is the only means envisaged in DO-178B/ED-12B for meeting those requirements. Replacing all testing at this level by formal analysis is not possible at this time; but formal methods can replace test for some properties, such as worst case execution time or stack usage. Formal methods can also be used to verify the compliance of the executable object code with respect to high level or low level requirements. However, testing will always remain mandatory and will be the primary means for verification of the executable object code.

Because formal methods cannot replace all testing, verification objectives for executable object code are the same when using formal methods as for test in DO-178B/ED-12B. However, an additional objective, as follows, is needed when formal analysis is used to verify properties of the executable object code:

• Analysis of property preservation between source code and object code. For the formal analysis of source code to be used as verification evidence for the target system, verification should be performed to establish property preservation between source and object code. By verifying the correctness of the translation of source to object code, formal analysis performed at the source code level against high or low level requirements can be used to infer correctness of the object code against high or low level requirements. This is similar to the way that coverage metrics gained from source code can be used to establish the adequacy of tests to verify the target system.

This allows for alternative verification paths for the executable object code, as shown in Figure 3. For example, compliance of object code to LLR can be demonstrated using formal analysis on source code and analysis of property preservation between source code and object code.

Verification of verification

Coverage analysis in DO-178B/ED-12B is defined in two steps:

requirements-based coverage analysis, to ensure that test cases exist for each requirement;

structural coverage analysis, to ensure that the code structure has been sufficiently exercised by test cases.

Fig 3. Alternative verification paths

Requirements-based coverage analysis can be done directly when using formal methods by showing that formal analysis cases exist for each requirement.

Structural coverage however is a notion strongly connected with test and execution of code. To be able to define an alternative to structural coverage analysis, the objectives of structural coverage analysis have to be examined. These objectives, as given in DO-178B/ED-12B, are to detect:

shortcomings in requirements-based cases or procedures, inadequacies in software requirements, dead or deactivated code.

When a code structure is not covered by some test cases, then either some test cases are missing for a given requirement, a requirement is missing, or the code structure is dead or deactivated.

When using formal methods, verification is exhaustive, so a requirement that has been verified formally has been completely covered. However, there is no guarantee that a requirement has not been forgotten. Thus, it is necessary to have a means to ensure the completeness of the set of requirements. Similarly, it is necessary to have a means to ensure that there is no unidentified dead or deactivated code.

Consequently, the solution proposed to provide coverage when using formal analysis at the executable object code level is meet the following set of fours objectives:

Complete Coverage of Each Requirement

The most thorough verification would be where all possible paths through the code with all possible data values are considered. Formal methods ensure this but sometimes the formal analysis requires assumptions to be made about the software system. All such assumptions should be verified.

Completeness of the Set of Requirements

Where requirements are formally modeled, it should be demonstrated that the set of requirements is complete with respect to the intended functions. That is:

• For all input conditions the required output has been specified.

• For all outputs the required input conditions have been specified.

If the set of requirements is found to be incomplete then additional requirements (generally not derived requirements) should be added. If a demonstration of completeness cannot be achieved, then structural coverage analysis must be used.

Detection of Unintended Dataflow Relationships

Verifying that the information flow in the source code complies with the requirements ensures that there are no unintended dependencies between the inputs and outputs of the code. If unintended dependencies exist then these must be resolved either by adding the missing requirements (generally not derived requirements) or removing the erroneous code.

Detection of Dead Code and Deactivated Code

Guidance for dead and deactivated code is not different when using formal analysis from using test.

In both cases, dead and deactivated code should be identified by review or analysis and dealt with as per the guidance in DO-178B/ED-12B.

Specific objectives

Previous sections have addressed how formal methods can satisfy the objectives currently defined in DO-178B/ED-12B. The proposed guidance for the FMTS also includes some additional objectives concerning the formal methods that are used.

When formal analysis is used to meet the verification objectives of DO-178/ED-12, the formal method should be correctly defined and justified as follows:

a. All notations used for formal analysis should be verified to have precise, unambiguous, mathematically defined syntax and semantics; i.e., they are formal notations.

b. The soundness of each formal analysis method should be justified. A sound method never asserts that a property is true when it may not be true.

c. All assumptions related to each formal analysis should be described and justified (e.g., those associated with the target computer; those about the data range limits; etc.).

The first objective requires demonstration that the method used is formal. The second one restricts the use of formal methods to sound methods. (Not all formal methods are sound.) The last one focuses on assumptions because assumptions are often used by formal analyses and it is important for the correction of the analysis that they are all justified.

Benefits of using formal methods

Formal methods were developed as a branch of computer science in order to reason more scientifically about software. Initially the advantages of formal methods were in analyzing the behavior of source code to understand where this was incorrect. Formalized requirements prevent misunderstandings that lead to error introduction. As development proceeds, compliance can be continually checked using a formal analysis to ensure that errors have not been introduced. A further advantage of using formal methods at the requirements level is the ability to derive or refine from these requirements the code itself, thus ensuring that no errors are introduced at this stage.

Alternatively their use at the requirements level allows formal analysis to establish correctness between requirements and code.

Improve Error Detection

Formal analysis can provide exhaustive verification at whatever levels it is applied: high level requirements, low level requirements, source code or executable. Exhaustive verification means that all of the structure is verified over all possible inputs and states. This can detect errors that would be difficult or impossible to find using only a test based approach.

Reduce Cost

In general, software errors are less expensive to correct the earlier in the development lifecycle they are detected. The effort required to generate formal models is generally more than offset by the early identification of errors. That is, when formal methods are used early in the lifecycle, they can reduce the overall cost of the project. When requirements have been formalized the costs of downstream activities are reduced. Formal notations also reduce cost by enabling the automation of verification activities.

Conclusion

A primary motivation for developing guidance for using formal methods in a certification context was to better enable the routine use of mature formal methods. That guidance, as proposed to date in a FMTS to DO-178/ED-12, allows adoption of formal methods into an established set of processes for development and verification of an avionics system to be an evolutionary refinement rather than an abrupt change of methodology. Formal methods might be used in a very selective manner to partially address a small set of objectives, or might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification.

This paper has presented a synthesis of the effort of the Formal Methods Sub-group of RTCA SC-205/EUROCAE WG-71 in developing guidance for using formal methods in these ways in a certification context with DO-178/ED-12.

Ongoing work in the formal methods sub-group concerns a discussion paper that is intended to give several examples of the use of formal methods.

Acknowledgement

This paper presents the work of RTCA SC-205/ EUROCAE WG-71 sub-group 6, we thank all members of SG6.

[1] RTCA/DO-178B, EUROCAE/ED-12B: Software Considerations in Airborne Systems and Equipment Certification, December 1, 1992.

[2] Advisory Circular # 20-115B. U. S. Department of Transportation, Federal Aviation Administration, issued January 11, 1993.

Accuracy & Consistency Compatibility with the target computer Verifiability Conformance to standards Algorithm accuracy Compliance Traceability Compliance Traceability Consistency Compatibility with target computer Verifiability Conformance to standards Partitioning Integrity Compliance Verifiability Conformance to standards Accuracy & Consistency Completeness and Correctness Compliance Robustness Compliance Traceability Compatibility Accuracy and Consistency Compatibility with the target computer Verifiability Conformance to standards Algorithm accuracy Compliance Robustness Compatibility with the target computer

  Analyses provide repeatable assessment of correctness. Reviews and analyses are used for all the verification objectives regarding HLR, LLR, software architecture and source code. Test is used to verify that the executable object is compliant with LLR and HLR. Test is always based on the requirements (functional test) and includes normal range and robustness cases.

	DO-178B/ED-12B identifies reviews, analyses and test as means of meeting these verification objectives. Reviews provide a qualitative assessment of correctness. System Requirements High-Level Requirements Source Code Executable Object Code Note: Requirements include Derived Development activity Review/Analysis activity Test activity Requirements Software Low-Level Architecture Requirements


C-E Gómez

J-C Pascal

P Esteban

Y Déléris

J-R Devatine

Embedded Systems Requirements Verification Using HiLeS Designer

Keywords: Verification, Validation, Virtual Prototype, VHDL-AMS, Petri-nets

One of the issues related to systems design is the early verification in first design steps: system specifications verification. Nowadays, it is common to use text-based specifications to begin a system design. However, these specifications cannot be verified until a software model is made. In this work, we show how can we use HiLeS Designer to model and verify, formally and by simulation an embedded system specification. This tool makes easier to build the model, using graphical concepts which are familiar to designers. It also helps to verify formally the structure and some logical behavior, and by simulation, it is possible to verify the consistence of the embedded system specification. We model and verify System Display Selector Requirements applying HiLeS Designer.

Introduction

In order to manage the complexity of a system, it is necessary to increase the abstraction level to describe in highlights how the system will be conceived before to take into account details such as specific time, protocols, and the partition hardware software. Electronic System Level (ESL) [Martin07] tries to introduce a new abstraction level called "System level" in the design flow of a system. This abstraction level is used to model the general functionality and architecture of the system without seeing detailed information and especially which system part will be developed in software and which part in hardware. The tendency in ESL is to create models based in traditional model language such as Java, C, C++ and more recently SystemC [IEEE05] and SpecC [START_REF] Fujita | The standard SpecC language[END_REF]. These models are verified by simulation using an specific test scenario. However this test does not guarantee the model can have a nonwished behavior, behavior that was not evaluated in the different test that the model is evaluated. There is another tendency to use model language such as UML [START_REF] Vanderperren | UML for electronic systems design: a comprehensive overview[END_REF] and SysML [START_REF] Friedenthal | A Practical Guide to SysML[END_REF]. These languages are tied to the MDA [START_REF] Boulet | MDA for SoC embedded systems design, intensive signal processing experiment[END_REF] in order to verify and to generate a virtual prototype base on the specification model created in these languages. We propose to use HiLeS Designer to model and verify embedded systems design representing textual requirements in block concepts where the functionality and the constraints are encapsulated into the block. HiLeS Designer has the feature to use Petri net as part of the model language. This feature allows to verify formally the structure and logical behavior described in this formalism without using a test scenario. HiLeS Designer also allows to generate an executable virtual prototype in VHDL-AMS where the analogical and logical behavior can be evaluated at the same time. This paper is organized as follows: Section 2 shows the related work with HiLeS Designer, Section 3 gives a HiLeS Designer overview. Section 4 describes how HiLeS Designer is used to model and to verify a System Display Selector. Section 5 provides the conclusions and directions for future works.

Related Work

In the market, there are different tools which use models of computation (MoC) concept to model systems in different domains. These MoC is the way to represent physical behavior of specific domains. For instance, image processing is modeled in a MoC called Kahn's Processes Networks, these are processes which interact by channels that can buffer messages (e.g. FIFO), or electrical circuits use Continuous-Time MoC which are functional and storage components communicating with continuous signals [START_REF] Liu | Responsible Frameworks for Heterogeneous Modeling and Design of Embedded Systems[END_REF]. Tools such as MLDesigner [START_REF] Schorcht | System-level simulation modeling with MLDesigner[END_REF], Ptolemy II [Ptolemy09] and Visual Sim [START_REF] Inc | VisualSim datasheet[END_REF] are examples that use MoC. There are other tools which use an specific language to describe the functional behavior of the systems. Matlab [Mathworks09], Modelica [START_REF] Fritzson | Modelica -A unified object-oriented language for system modeling and simulation[END_REF] and Cofluent Studio [START_REF] Calvez | Real-Time Systems a Specification and Design Methodology[END_REF] are examples of this tendency. Matlab uses a C-based language to describe a system, Modelica use its own orientedobject language to model and Cofluent Studio is based on SystemC. Some of this tools allow the mix of MoC. In MLDesigner, it is possible to model in the same workspace continuous-time and Discrete events MoC; it also is possible to build in Matlab/simulink/Statechart mix but its execution is done in its own execution engine, e.g., there is communication transformation between the two MoC in order to execute in its own domain. HiLeS designer contains Continuous-Time, Discrete-Time and Discrete event MoC, thanks to the use of VHDL-AMS as base of the HiLeS formalism. VHDL-AMS allows modeling Continuous and Discrete time systems, but it is not appropriated to model Discrete events systems. For that reason, we transform the discrete-event model to VHDL-AMS in order to execute in a same environment the three MoC. This transformation gives HiLeS Designer the advantage of simulating faster and creating, in one standard language, Intellectual Properties (IPs).

HiLeS Designer

HiLeS

High Level Specification or HiLeS is a graphic language developed by Jimenez [START_REF] Jimenez | Spécification et conception de microsystèmes basés sur des circuits asynchrones[END_REF]. Its objective is to help systems designers to model the architecture and behavior of a system into system level, e.g., without specifying software and hardware features. HiLeS has four main concepts:

• Structural Block • Functional Block • Control Net • Channels • Ports
The structural block represents the system architecture. Each structural block can be composed by other Structural blocks, functional blocks and a control net. These elements represent a specific group of behaviors encapsulated in a block. The system hierarchy is decomposed in structural blocks and, at the same time, the detail level. The functional block is the lowest level in a system functional description. It defines a function represented by an equation. The Control Net is an ordinary Petri net which controls the execution sequence of each block defined in the model. Each block is represented by a place in the control net. By arcs, drawn with dashed arrows, the process defined in the related block is executed. Once the process finishes, the block fires the transition after the place which represents the executed block and the control net sequence continues. Channels are routes which transmit the information from the environment to the system, from one block to another and from the control net to blocks. There are defined two channel types: Control and Continuous. The Control channels manage the execution of the blocks, and the Continuous Channels route the signals from blocks to blocks or environment to system, according to their nature. Finally, ports are interfaces between the blocks and its environment. They put the blocks or the environment information within channels in order to transmit or receive information (out-port and in-port respectively) to other blocks or environment. They have nature and type such as they are defined in VHDL-AMS.

In Figure 1 In this example, the first hierarchical level is represented by the "Structural_1" block. This block is internally described by two functional blocks (Functional_0 and Functional_1) and these blocks define the "Structural_1" block functionality. The "Structural_1" intern definition is considered as the second hierarchical level an it is the last level because there are only functional blocks. The signal flow is represented by the signal transformation made in the structural and functional blocks flow. In the example, there are two signals continuous that go from the environment to the system through A_1 and A_3 channels. These signals are transformed inside "Structural_1" structural block. The signals go in though P_2 and P_3 in-ports. Inside the structural block, the signals are conduced by A_2 and A_4 channels to the "Functional_0" block where they are processed. The result is only one signal which goes out though P_4 out-port. The new signal is conduced from the "Functional_0" block to "Functional_2" block through A_5 channel. This signal is processed for "Functional_2" functional block through P_0 in-port. The final result goes out through the P_1 out-port and it is transported to the P_4 out-port through A_8 channel. The resulting signal is sent from "Structural_1" through P_4 out-port to the environment using P_2 out-port conduced by A_8 channel.

The sequence flow is represented by the control net. A token in a place indicates which block is in execution. In the example, the execution begins in Pl_0 place. When Tr_0 transition is fired, a token is sent to Pl_1 and another to execute "Structural_1". Then, inside "Structural_1", Pl_3 is marked. The sequence continues, executing "Functional_0". Once "Functional_0" finishes its process, Tr_3 transition is fired by a signal from the functional block. The sequence continues in the same way finishing in Pl_2. For each structural block is possible to create different architectural solutions as it is depicted in Figure 2. Figure 2a shows the structural block with its in-ports which process the signals from the environment and out-ports that are the processing result. This structural block has a specified functionality. However, to solve this functionality it is possible to propose different solutions. Figure 2b and 2c shows two different architecture examples in order to compose "Structural_2" block.

HiLeS Designer

HiLeS Designer is the tool that supports the HiLeS language and it was conceived by Hamon [START_REF] Hamon | Méthodes et outils de la conception amont pour les systèmes et les microsystèmes[END_REF]. In Figure 3, there is a schema of how HiLeS Designer works. The designer interprets and represents in HiLeS concepts the specifications described in natural language. The model is built not only with the HiLeS concepts, but also with VHDL-AMS description in the functional blocks. Once the model of the first executable level is created, e.g., the first level abstraction, it is possible to verify before continuing with levels more detailed. HiLeS Designer has two types of verification, formal logical verification and verification by simulation. Formal logical verification is a process related to the control net described in the model. Since the control net is a Petri net, it is possible to verify mathematically the structure and the behavior of the execution sequence design. Features such as deadlock (when a marking is not enabled to activate a transition), liveness (when the Petri net is not blocking), boundedness (when the tokens in each Petri net place is limited in every marking) and reachability (when every place is reachable) are analyzed. This process is presented in HiLeS Designer due to the integration with a Petri net analysis tool call TINA [START_REF] Berthomieu | Time Petri Nets Analysis with TINA[END_REF]. HiLeS Designer extracts the control net from the model which wants to be analyzed, it translates the control net to the TINA language and create a flat text file. HiLeS Designer executes TINA with this file and TINA generates a flat text file with the analysis results. HiLeS Designer reads the file and prints in a output text field. With these results, the designer identifies the logic problems in its design without need a test bank to find them out. When the logic verification is made, the verification by simulation is executed. HiLeS Designer generate a virtual prototype from the model in VHDL-AMS. Each concept from the HiLeS language is connected to a concept in VHDL-AMS. At the same time, the test scenario is created according to the designers' configuration. The VHDL-AMS code is compiled and executed in VHDL-AMS tools such as SystemVision [START_REF]Mentor Graphics[END_REF]. The designer analyzes the simulation results and compares if these results are according to the specification. Once the first level is verified, the designer can descend the abstraction level to model in more detail the system.

System Display Selector

In order to show how HiLeS designer works and it is applied in a real system, we present this example. The example system is modeled using HiLeS Formalism starting from the specification document. The formal verification and the verification by simulations are applied.

SD Selector Modeling on HiLeS Designer

The System Display Selector (SD Selector) is a device which is used in Airbus aircraft. This system selects the correct page to be displayed in a screen according to their input signals. The system requirements are described in natural language in a document. The work is to interpret the system requirements, to build a model and to verify the model coherence and completeness satisfying the requirements. This verification is done formally and by simulation using HiLeS Designer. To model the system in HiLeS Designer, we have to use different abstraction levels in order to make step by step the model based on the textual requirements. The first level, called "Level 0", serves to model the system and its environment as a black box (Figure 4). The environment is used to model different scenarios that the system can have following the textual requirements. This scenario model helps to generate the test scenarios for the virtual prototype in VHDL-AMS.

Figure 5: System Architecture requirement. The following levels are made based on the architecture proposed by the textual requirements. In Figure 5, there is an architecture example described in the system requirements, and in Figure 6, the same architecture expressed on HiLeS. We also maintain the hierarchy expressed in the requirements document, using the structural block concept in HiLeS. Additionally, to make easier the functional description with more detailed requirements, we build new hierarchies to specify each functionality, until we reach to the lower level of description using functional blocks. In order to show in more detail how a model can be built using the HiLeS formalism, we choose the "Valid key Action" subsystem. The subsystem's functionality evaluates the user's action on the keyboard, when the user selects the information they want to show on the screen. The "Valid key Action" subsystem requirements are described in a requirement document subsection. The textual requirements are interpreted and the subsystem model is deduced. In Table 1, there are some requirement examples extracted from the document. In Figure 7, the HiLeS model of this subsystem is depicted. This model follows every requirement described for the subsystem in the requirements document. To illustrate how the textual requirements are interpreted using HiLeS concepts, we will use the requirements described before. The state position presented in the Requirement 1 is represented by the places Pl_170 (Pressed) and Pl_66 (Released). The state Status is represented by the places Pl_179 (Valid) and Pl_178 (Invalid). According to the user's action, the states change. Following the Requirement 3, when a key is pressed in a keyboard, the place Pl_64 is filled by a token. Since the Pl_66 (Unpressed) and Pl_64 (PressKey) have token, the Tr_61 is fired, then the Pl_68 (Timer) and Pl_170 (Pressed) is filled with a token. That means the key status changes from "released" to "pressed" achieving the textual requirement. The requirement 2 is identified in the figure by the token presented in the places Pl_66 and Pl_179. The timer, which is a functional block, is described in VHDL-AMS (Figure 8) and its behavior is to wait a defined time period. In our example, the time is the period where the pressed key is valid without releasing it.

Formal Verification Analysis

Once the model is complete, the model verification can be started to ensure the requirements are considered. The first verification step is the formal verification. Its purpose is to find inconsistencies in our design (Blocking, deadlocks, behaviors which are not taking into account in the requirements). In this paper, we choose the requirements 4 and 5 to verify partially the model. These requirements are represented by the actions on the Places Pl_71 (Selected), Pl_170 (Pressed) , Pl_179 (Valid) and Pl_178 (Unselected or None) in Figure 7. The initial state of the keys shall be status VALID and position RELEASED.

Req. 3

While the system receives an action on the keyboard, the corresponding key position shall be set to PRESSED.

Req. 4 SELECTED KEY shall be the identifier of the first PRESSED AND VALID key.

Req. 5 If there is not a (PRESSED AND VALID) key then SELECTED KEY shall be set to NONE. To evaluate the behavior of the model, Table 2 is built with the cases that are tied to the requirements 4 and 5.

As an example, to verify the requirement 5 it is necessary to consider: if "Pressed" or "Valid" has a token, or if neither "Pressed" nor "Valid" has a token, then the place "None" must have a token. The formal verification is based on Petri net accessible markings search. The behavior of this requirement is verified by lines 0, 1, 4, 5 and 6 of Figure 9.

Finally, we can find others cases that are not taken into account in Table 2. For example, the lines 2, 9 and 10 show other cases that are summarized in one: "Pressed", "Valid" and "None" have tokens. This case is identified when the transition that changes the key status from "None" to "Selected" is not fired yet when there is a token in the places "Pressed" and "Valid". The formal verification can show that some requirements are missing; for instance, if some combinations of states are found but not initially defined. On the other hand, some requirement inconsistencies can also be shown during the modeling process.

Req

Verification by simulation

Following the verification process, the second step is to simulate the system model in order to verify the requirements which could not be verified by the formal analysis (operations sequences, temporal constraints, ...). HiLeS Designer is used to generate a virtual prototype in VHDL-AMS, transforming the system model to VHDL-AMS. This transformation is made automatically by HiLeS Designer. The tool generates the prototype and the test scenario source code in one step. The test scenario is generated according to the scenario defined in the HiLeS environment model and then SystemVision is used to simulate the virtual prototype; the results are shown in Figure 10. This scenario is related to specific requirements defined in the requirements document and the behavior is verified by the simulation.

The model formal verification helps to identify all the cases defined by the requirements.

Figure 10 shows the action to press and release a key in 2 seconds. The initial key state is "Released" and "Valid", as the Requirement 2 defined. In the first signal, the pressing key event is a pulse. At the same time, the position state changes from "Released" to "Pressed" (Requirement 3) and the status state continues being "Valid", following the

  , we show an example of the HiLeS graphic representation. The figure illustrates two flows: signal flow and sequence flow and also two hierarchical levels.

Figure 1 :

 1 Figure 1: HiLeS Concepts example

Figure 2 :

 2 Figure 2: Different architectural solutions.

Figure 3 :

 3 Figure 3: HiLeS Designer functionalities

Figure 4 :

 4 Figure 4: Level 0 of the SD Selector model

Figure 6 :

 6 Figure 6: System Architecture requirement in HiLeS.

Req. 1

 1 Each key shall be associated to two couples of states: Position: PRESSED-RELEASED and Status: VALID-INVALID Req. 2

Figure 7 :

 7 Figure 7: Valid Key Action Model in HiLeS

Figure 9 :

 9 Figure 9: Accessible marking in the "Valid Key action" subsystem.

Table 1 :

 1 Part of System Requirements

Table 2 :

 2 Cases to evaluate the requirements 4 and 5.

Requirement 4. Also, the key action state changes from "None" to "Selected"; this means the key pressed is selected. When the released event is done after 2 seconds (second signal), the valid position changes from "Released" to "Pressed", and the key action from "Selected" to "None". The result of this simulation satisfies the system requirements. Finishing the verification process, we can conclude our model agrees to the textual requirements because all of them are correctly considered.

Figure 10: "Valid Key Action" Subsystem simulation based on a scenario.

Conclusions and future work

HiLeS Designer is a tool that follows the conception of new methodologies in ESL. We explained the formalism that this tool uses, its features and an Airbus system study case developed on HiLeS Designer. We developed an executable and verifiable model starting from the Airbus' textual requirements until we arrived to an executable virtual prototype in VHDL-AMS. We showed the practical HiLeS Designer use on verifying formally the logical structure and verifying by simulation the temporal constraints, behavior and logical sequence against each textual requirements of the SD Selector System. We also presented the possible risks (deadlock, non-liveness, non-boundedness) that a logical structure model can have if a formal verification is not applied. In the future, we will work in the transformation from standard language such as UML and SysML to HiLeS in order to verify and to execute models described in these languages. We will use the MDA transformation concepts to achieve this objective.