Andreas Korff
email: andreas.korff@artisansw.com

AUTOSAR and SysML -A Natural Fit?

Keywords: AUTOSAR, SysML, Model-based Development, Domain-specific Modeling, Visual Modeling, UML

published or not. The documents may come

Current Situation

All current functional implementation solutions for automotive electrical and electronic development are proprietary. It is therefore quite difficult to exchange functions and applications between automotive OEMs and suppliers. If this type of development process structure continues, the foreseeable future growth in functional complexity will result in the need to invest increasingly more manpower while sacrificing complete control of the development process.

Modern cars have reached an exceptionally high level of functional complexity. Driven by new legal safety and environmental regulations, in addition to customer feature demands, automotive functionality requires ever more complex software and electronic components, which must be very closely coupled in a network structure to perform completely and correctly.

AUTOSAR

The AUTOSAR Initiative

In July 2003 the AUTOSAR (AUTomotive Open System ARchitecture) partnership was formally launched by its core partners: BMW Group, Bosch, Continental, DaimlerChrysler, Siemens VDO and Volkswagen. Afterwards Ford Motor Company, General Motors, PSA Peugeot Citroën and Toyota Motor Company become core partners as well. Since inception, many other OEMs and automotive suppliers have joined AUTOSAR as premium members. Core and premium members assign resources to the different working groups within AUTOSAR. Associate members are allowed to view finalized documents in advance to the public. Development members can be nominated to participate in the AUTOSAR working groups.

Objectives

The AUTOSAR initiative will define standards, on which the implementation of future automotive applications will be based. By following these standards, it will be possible to manage the growing E/E complexity of the development of automotive functionality. This will also result in greater flexibility for product maintenance, enhancements and updates. The solutions based on the AUTOSAR approach will be scalable in and across product lines. In addition, the exchange of functions between OEMs and suppliers will be possible. All domain areas in automotive will be addressed: Powertrain, Chassis, Safety, Multimedia/Telematics, Body/Comfort and Human Machine Interface. The automotive customer will therefore get cars of higher quality with more reliable electronic components.

Three main topics have been defined:

• A basic software core • Standardized functional interfaces and • Methods for software integration.

Technical Concept of AUTOSAR

Figure 1: The AUTOSAR Approach AUTOSAR will define a common software infrastructure based on standardized interfaces. This will include a standardization of different API's, resulting in the separability of the AUTOSAR software layers. An encapsulation of functional software components will be defined as well as the data types of the software components. In order to allow these software components to work, the software infrastructure including basic software modules will be identified and specified. These basic software modules will have standardized interfaces. Partitioning and defining the best resource usage will therefore be possible, while still allowing local optimisation to meet specific non-functional constraints.

Figure 2: The ECU Architecture

The AUTOSAR software architecture consists of a layered design: Figure 1 shows this as a UML Structure Diagram. Above the ECU-Hardware, the Basic Software provides services to the AUTOSAR Software Components. Inside the Basic Software, there are four different elements:

• The Services including RTOS services. Since the definition of an RTOS is not considered as a goal for AUTOSAR, existing RTOSes will be taken into account here. The basic Services also include communication functions for all relevant vehicle buses like FlexRay, CAN, MOST or LIN. • The Microcontroller abstraction which interfaces to the • ECU abstraction and • Complex Device Drivers, which allows direct access to Microcontroller-specific hardware, so complex sensors or actuators with specific functional and non-functional requirements can be implemented. The overall design concept in AUTOSAR is the separation of application and infrastructure. An application is formed by the connection of different AUTOSAR software components. An example is given in figure 3. As seen in the example, the AUTOSAR software component is the most important structural element. Similar to the UML 2 components, the AUTOSAR software components contain -here unique-ports to interact with their outside world. Also in AUTOSAR required and provided interfaces are defined. These are connected to the ports, which are either PPort when their interface provides data or services, or RPort when a interface is required. AUTOSAR goes beyond UML 2 to define interfaces as either "Sender-Receiver" or "Client-Server". A Sender-Receiver-Interface provides or requires data, whereas a Client-Server-Interface defines services. UML 2 stereotypes together with appropriate constraints are a promising way to support this. An example of a Client-Server connection is shown in Figure 4.

«AUTOSAR Software Component» client2 «AUTOSAR Software Component» server «AUTOSAR Software Component» client1 Service_requested «ClientServerInterface» Service_provided «ClientServerInterface» Service_requested «ClientServerInterface» Figure 4: Client-Server communication
The AUTOSAR sender-receiver communication always exchanges data asynchronously and in a non-blocking manner. New symbols can and should be used to quickly communicate this to those who read the diagrams. This is shown in figure 5. Note: Since the interface symbols "ball" and "socket" currently couldn't be replaced graphically, the synonym Interface dependencies defined within the UML have been used here. The size of an AUTOSAR software component is not defined. However, a software component is atomic, as such it cannot be divided and thus cannot run on several ECU's. In a UML model, this can be achieved by defining a 1:1 relationship between the software component and the appropriate ECU. Although an AUTOSAR software component is designed independently from the available infrastructure, its interface, functional and nonfunctional constraints must be described. Within AUTOSAR, the format and structure of the software component description has to follow the definitions of the so-called software component template. This guarantees that the description contains all the necessary information, such as the operations and attributes that the software component requires or provides to other components. In addition, the infrastructure requirements, the hardware resources needed, and specific implementation details to be followed, are specified in the software component description. If an AUTOSAR software component is implemented, this implementation is independent from the specific ECU (or the Microcontroller architecture within the ECU) to which the component is mapped. Even the software components that are needed to get the necessary data or functionality don't have to reside on the same ECU. Additionally it is possible to have multiple instances of the same software components running. There are specific AUTOSAR software components for sensors or actuators. These generally run on the ECU that the sensor or actuator is physically connected to, and encapsulate the physical nature of the sensor output or actuator input. The technical details of the ECU and its Microcontroller(s) are hidden as usual -the Sensor/Actuator software component depends on the sensor or actuator for which it is designed.

Virtual Functional Bus

In order to make AUTOSAR Software components relocatable, the concept of the Virtual Functional Bus (VFB) has been developed. Using software component descriptions as input, the VFB validates the interaction of all components and interfaces before software implementation. So the integration can be tested much earlier than today. Within the VFB, all necessary connectability between AUTOSAR Software Components is abstracted, independent from their future location in the vehicle. So if two components have to communicate, this can be specified even without the knowledge of the specific hardware on which these software components are running. Also the communication needs of an AUTOSAR Software Component are fulfilled within the VFB in an abstract manner (using its underlying layers like OS or hardware drivers).

Well-defined communication patterns within the VFB provide the abstract communication services. The realization within the different ECU's is done by the AUTOSAR Run-time Environment (RTE) after the onto the existing hardware. Within the RTE, the communication functionality is implemented in the Basic Software and its communication means. Figure 6, a graphically stereotyped UML composite structure diagram, shows the elements that can be connected via the VFB. Only the Complex Device Drivers and the ECU abstraction are specific to the Hardware used.

Technical Artifacts

In order to build up systems using the concepts of AUTOSAR, several artifacts have to be created. First every AUTOSAR Software Component will be described by its Software-Component Description. This is XML-based and includes detailed definitions of the ports, interfaces and connections between the Software Components. ECU descriptions, also in XML format, will describe the available resources. In addition, the System Constraint Description will give additional information about the constraints given by an already existing network architecture. This software to hardware mapping should be done with tool support.

UML 2.0 and its extension mechanism

When cross-referencing the ideas of UML and AUTOSAR, it is obvious that UML 2 and AUTOSAR use similar concepts, e.g. components, ports and interfaces, which are defined in the UML class model for composite structure diagrams. Therefore the UML 2 syntax can be used directly for the system description within AUTOSAR. However, some concepts in AUTOSAR require the adaptation of UML to fit to the AUTOSAR syntax. A UML Profile for AUTOSAR is necessary, which adds all AUTOSAR specific information and containers into UML 2. Some have been defined in the figures in this paper using the graphical adaptability of ARTiSAN Studio 6.0. Since the Meta model of AUTOSAR is based on the UML 2.0, the first step to make a UML tool like e.g. ARTiSAN Studio AUTOSAR-compliant is defining additions to UML specifically for AUTOSAR within an AUTOSAR Profile. Then developers can use a tool like ARTiSAN Studio to describe AUTOSAR compliant software by using the domain-specific terms and graphical elements. In order to support domain-specific modeling even further, it is necessary to be able to specify rules for modeling. This enables the user to avoid modeling errors from the beginning or helps him by adding e.g. AUTOSAR-specific elements or structures automatically to the manually edited model elements. ARTiSAN Studio 6.0 includes this capability by the possibility to add scripts to those UML stereotyped extensions, which can also be used to restrict the modeling activities to the connections and properties allowed in AUTOSAR.

SysML

The AUTOSAR structural definitions base on UML 2.0. In parallel, the OMG started a Request for Proposal in March 2003 to define a UML-based modeling language for Systems Engineering. Currently two teams, the SysML partners and the SysML Submission Team are working in parallel to meet the schedule to finalize the SysML specification by Q1 2006. The SysML is defined to be a graphical modeling language For Systems Engineering in response to the requirements developed by the OMG, INCOSE, and AP233. It re-uses a subset of UML 2.0 and add extensions to it, thus supporting the specification, analysis, design, verification and validation of a broad range of complex systems. The systems may include hardware, software, data, personnel, procedures, and facilities. SysML complements the UML 2, so both Systems Engineers using the SysML and Software Engineers working with UML 2.0 can seamlessly cooperate using the same graphical language with different characteristics.

«userModel» XYZ Model «metamodel» UML «metamodel» SysML «modelLibrary» SysML Profile «metamodel» MOF «import» «instanceOf» «instanceOf» «reuse» «instanceOf»

The SysML Profile Structure

In order to extend the UML 2, the SysML defines a SysML Profile. This is divided into several subpackages.

Figure 9: SysML Profile structure

The sub-profiles, stereotypes and tag definitions defined in the SysML Profile extend the existing meta model elements of UML 2.

SysML Graphical Notations

The In order to understand the focus of the SysML better, let's have a look on the new diagram types. They explain the gaps for systems engineering within the UML 2. This existing modelling language already incorporated very important structural modelling capabilities like structural sequences and composite structures. However, especially the ability to use and model requirements is essential for systems engineers. The frame itself represents a constraint block, the pins on the frame show parameters. In the constraint block there is the possibility to include other constraint blocks. The constraints can be linked to blocks. So flows are supported as well, i.e. flow properties, flow items and flow ports. The SysML definition for flows extends the UML 2 information flow. The activity diagrams are enhanced within the SysML to include the continuous item flows, so the behavior of elements are better and completely described.

Conclusion

The AUTOSAR initiative shows how domain-specific modeling for automotive modeling can be defined to standardize concepts, interfaces and services. This will be specified based on the UML 2.0 using a UML Profile for AUTOSAR. All necessary constructs for software components, system constraints and system definitions will be included. However, taking into account the generic systems engineering requirements for modeling complex systems, these can be used in automotive modeling as well. The SysML closes the gaps between systems and software engineering by streamlining and extending the UML 2 concepts to fit better for modeling systems of systems.

Figure 3 :

 3 Figure 3: Example application, consisting of connected software components

Figure 5 :

 5 Figure 5: Sender-Receiver communication

Figure 6 :

 6 Figure 6: Hardware Interaction

Figure 7 :

 7 Figure 7: Atomic Software Components and AUTOSAR Services connected to the Virtual Functional Bus

Figure 8 :

 8 Figure 8: Embedding of SysML and SysML models into UML 2.0 Since the work on SysML is not finalized yet, the concepts and ideas presented here contain the status of the on-going work today, in November 2005. They may change until the final SysML specification is released.

Figure 10 :

 10 Figure 10: SysML Diagram Taxonomy

Figure 13 :

 13 Figure 13: Constraint Block Example

  Figure 14: Activity Diagram Example

  SysML does not use all the thirteen diagram types defined in the UML 2.0. Instead it uses its own diagram taxonomy, where two new diagram types are introduced:

	• Requirement Diagram
	• Constraint Diagram
	Some structural diagram types are defined in a
	simpler way compared to the UML 2 to reflect
	systems engineering concepts better. Also some
	diagram type names have been changed.
				«Diagram Type»
				SysML Diagram
		«Diagram Type»	«new Diagram»	«Diagram Type»
		Structure Diagram	Requirements Diagram	Behavior Diagram
	«modified Diagram»	«modified Diagram»	Use Case Diagram	Timing Diagram
	Block Definition Diagram	Internal Block Diagram
			Instance Diagram	Sequence Diagram	State Machine Diagram
	«new Diagram»
	Constraint Diagram
			same as UML 2		«modified Diagram»
			Object Diagram		Activity Diagram
	Simplified	Parametric Diagram
	Class Diagram	in SysML v0.9
			Derived from UML 2.0
			Composite Structure Diagrams

  The UML 2 only uses eventbased modelling, which is enough for the software perspective. To build up a system also using the systems engineering perspective, it is additionally needed to be able to use e.g. physical equations.

	elements to describe requirements completely. This	systems modelling.
	includes the requirements properties like e.g. name,
	ID, requirement descriptions and others. Additional
	the requirement dependencies like the fact that one
	requirement is derived from others or a requirement
	contains other requirements can be graphically
	shown. The really new -and important-modelling
	capability is that the requirements can be linked to
	other modelling artefacts like system elements from
	the system design or test cases. This is done using
	stereotyped dependencies like <<verify>> for test
	cases or <satisfy>> for design elements. The fact to
	have all three perspectives, requirements, design
	elements and tests, in one model will empower the
	user to trace down any missing link between these
	three worlds. If there is a requirement, which is not
	satisfied by at least one design item or which does
	not have a link to a defined test which can verify it,
	this can be automatically analysed.
	The next new concept within the SysML is the
	notation of blocks. Similar to the UML 2 components,
	the block are not restricted to software components.
	They represent a module which can be at any level
	in the system hierarchy, including external systems,
	logical or physical subsystems, independent if
	consisting of software and/or hardware. Blocks can
	be used for black-box or white-box modelling.
	Block definition diagrams are simplified class
	diagrams from the UML 2. They use the composition
	association, now between blocks.
	def System Blocks
	«block»	1	1	«block»
	Tank	sink		Water System	req VehicleSystemRequirementsFlowDown
	«flowPort» {in}	1	1	sourceFlow : Water	«reqDocument» MarketNeeds			VehicleSystemUseCases
	liquidIn : Liquid	source		sinkFlow : Water
	«flowPort» {out} liquidOut : Liquid			1			«requirement» «trace»	«rationale» Ref: Statement of Work «trace»	UCD uc Driver	Drive Vehicle
							Vehicle System Specification
				1	pump
				«block» Pump	«requirement»	«requirement» R111	«satisfy»	Vehicle System Design
	«profile» SysML «profile» Blocks	«profile» Activities		«flowPort» {in} pumpedIn «flowPort» {out} pumpedOut	«profile» ModelElements	VehicleAcceleration «requirement» {id# = 102; txt = System shall accelerate from 0 -	id# txt System shall ... 111 «deriveReq»	id# = 111	«block» Vehicle 1 1 1	1	brake
	«modelLibrary» Units	«modelLibrary» ControlValues					60 mph in lest than 8 seconds under the specified ...		«rationale»		«block» Power Train	«block» Brakes
									Ref: Trade Study
	Figure 12: Block Definition Diagram	Power Subsystem Specification «requirement»	«satisfy»	Power Subsystem Design (Alternative=V6)
	«profile» Flows The internal block diagrams are stereotyped «profile» ConstraintBlocks «profile» Allocations «profile» Requirements composite structure diagrams. The compositions	«requirement» {id# = 337}	«requirement» {id# = 340}
	already modelled in the block definition diagrams are	R337		R340
	re-used. However, the internal connectivity is added in this diagram form.	«verify» Engine Horsepower Test «testCase»
	The next new diagram within the current SysML	Figure 11: Requirements Diagram
	definition is the constraint diagram. Within the
	version 0.9 of the SysML profile, it was called parametric diagram. The reason behind this addition to the UML 2 is the necessity to include time-	Within automotive development, the success of requirements management tools show the big need of this engineering perspective. Within the SysML, it
	continuous modelling and physical equations into the	will be possible to use a standardized set of profile

Glossary


Matthew C Hause
email: matthew.hause@artisansw.com

Francis J Thom
email: francis.thom@artisansw.com

Modelling Distributed Integrated Modular Systems Using the UML™ and the SysML™

Keywords: Integrated Modular Avionics, SysML, Blueprint, UML, MDA

 and the evolving ASAAC Standards [Ref 2] this paper will elaborate currently available support for documenting the architecture of: highly distributed real-time systems, the communication mechanisms between applications or components and capturing the properties required to indicate how they are scheduled. This paper will examine the exploitation of this design information to address, amongst others, the safety assessment of a single configuration (a set of applications or components), the assessment of run-time reconfigurations, the generation of 'blueprint' files to configure the Hardware, and the Operating System, and to manage the run-time distribution (and re-distribution) of applications. In essence this paper will elaborate a method of creating a single-source repository for all the design information (building on the Unified Modelling Language UML [6] and Systems Modelling Language [7] Standards) fit for the demanding requirements for IMS.

Federated or Networked Architectures?

It is useful to start with a definition of terms, specifically, architectures. "The software architecture of a program or computing system is the structure or structures of the system, which comprise software elements, the externally visible properties of those elements, and the relationships among them." [START_REF]Software Architecture in Practice[END_REF] To elaborate further, software architectures are a complete abstract representation of a system-wide solution. Software architectures contain collaborating software artefacts that are essential both to the comprehension of the proposed solution (model) and the construction of the end product (executable). Software artefacts are defined in terms of their roles, responsibilities, connectivity, interfaces, behaviour and persistence with other artefacts within the same architecture. Software architectures also define the control of concurrency and eventual deployment of the software artefacts (especially within multithreaded n-tier distributed solutions). Software architectures may contain in part, or in totality, axiomatic solutions -patterns, frameworks and components -to localized elements, or the whole problem. Software architectures may exhibit idiomatic constraints (technical and non-technical) peculiar to the problem-domain (implementation language, re-use criteria, safety-criticality, robustness, production time, cost and availability). This definition does presume the existence of (at least one) other architectural model, the physical architecture (hardware and its connectivity) upon which the software artefacts, are deployed. Basically, the software architecture is the solution to the problem from the software perspective, the physical architecture being the solution to the problem from the hardware perspective. Federated Architectures. Although predominantly applied to avionics systems, the overarching philosophies behind IMS, supported by both ARINC-653 and ASAAC, are applicable to a much wider domain of systems and software development. Fundamentally IMS is a logical progression from federated system architectures with centralized control to wholly modular system architectures. 1, depicts a number of Line Replaceable Units (LRU's) (e.g. a Radar, an Inertial Navigation Unit (INU)) forming a federated union, typically via a set of communication networks (e.g. MIL-STD-1553B [START_REF]Interface Standard for Digital Time Division Command/Response Multiplex Data Bus[END_REF] data bus) with a central LRU (e.g. a Mission Computer) that manages and coordinates the federated union. Although the majority of avionics systems in service today employ this architecture it is not without its problems. Replacing a LRU is not as simple as its name suggests. Although standards exist for interface specifications for some LRU's (e.g. the SNU-84 Specification for INU data formats), typically suppliers of LRU's enhance the capabilities and therefore extend the interface specification. For example, by adding new messages and data formats or a different physical connector beyond that called for in the standard 1 . If a systems engineer wishes to make use of these 'nonstandard' capabilities, the simple act of replacing the LRU is compounded by the changes required to the Mission Computer, in this example, to interpret new messages and changes to the physical connector (and internal wiring). Even in this very simple example, the high degree of coupling between the Application and the Interface to the LRU's; can adversely impact the cost of maintaining existing systems, maintenance, hardware obsolescence and the propensity to use new capabilities defined for an LRU,. In some cases, due to the long lead times involved, this can also impact the initial development of the system due to re-work 2 . [START_REF]CORBA Specification[END_REF]). This architecture handles failure of processing elements, with the OSL re-configuring the distribution of applications across the remaining processing elements. In future implementations, the AL could be re-configured (without a failure)swapping one set of applications for another from a list of available configurations -where the new set of applications may exhibit a different set of capabilities provided to the end-user. For example, one configuration may exist to support a combat aircraft during a surveillance role and this may be swappedout for a different set of applications to support an air-to-air combat role. So, re-configurations are not just to address the issue of failure, they are also required for normal use. In an IMS, the blueprints are of paramount importance. Get this wrong and the whole system may catastrophically fail. Model Driven Architecture. These problems are the many of the drivers behind the Model Driven Architecture (MDA) initiative by the Object Management Group (OMG) who oversee the Unified Modelling Language (UML). "Model-Driven Architecture (MDA) is an approach to the full lifecycle integration and interoperability of enterprise systems comprised of software, hardware, humans, and business practices." [START_REF]Model-Driven Architecture and Integration Opportunities and Challenges Version 1.1 Desmond DSouza[END_REF] At the heart of the MDA are three models: the Platform Independent Model, (PIM), The Platform Specific Model (PSM), and the Generated Application. The Platform Independent Model expresses the system intent independently of any implementation technology. Regardless of the platform on which the system is implemented, this model will be valid. It will comprise the many different system viewpoints described earlier. The Platform Specific Model is created from the PIM and expresses functionality in a technology-dependent fashion.

Finally, the Generated Application is created from the PSM. To Continue. The rest of this paper will concentrate on the design and documentation of the AL, but also looks at the OSL to elaborate how UML and SysML can be used to capture the information required to construct an IMS, and more importantly how to capture the information required for validating and generating the run-time blueprints. Work is currently underway to perform verification and validation of blueprints and, as will be described here, the bulk of the information for these activities can be captured within a UML model.

Modelling IMS Application Capabilities

No guidance is given for the 'role' of an individual application that, collectively within a configuration, is both maintainable and performance-efficient. Guidance is given to ensure that some form of health monitoring, security management, fault management and re-configuration for the OSL exists. The selection of application partitions is left up to the designers of the application layer. It is suggested here that the applications are identified in the same way as 'objects' in an object oriented (OO) design.

Given the strong parallels between IMS architecture and the OO paradigm, it seems that the UML would be an obvious way of visualising an IMS. More simplistic notations being inferior to the UML in expressing the multiple perspectives required to conceptualise a complex network of interrelationships between applications, processes and threads to support information and control flow throughout a dynamically distributed and layered architecture. Further to this, the ability to extend the UML notation (through profiles) ensures that IMSspecific properties can be captured in one place and maintained within a single-source repository. Profiles. Profiles are the means by which users can customize UML for specific applications and domains. A UML profile is a coherent set of stereotypes, constraints, tag definitions, and tagged values, defined for specific purposes. [START_REF]UML 2.0 Specification[END_REF]. If we group common requirements stereotypes together into a collection, we can create a requirements profile. An IMS profile is what we are proposing for facilitating the goals defined in this paper. Conflicting Drivers. There are two, at times, conflicting heuristics at work during the development of an IMS application layer. The first is to make the 'role' of an application unique, such that it does one thing well. This also facilitates maintenance making it easier to identify where a change should be made when a role of the carrier vehicle is changed. Furthermore, when re-configurations are requested 'roles' are easier to switch-in and out compared to functionality that may be highly coupled with external LRU's. The second is that each application executes as its own executable thread (or pseudo thread). Time must be allocated for elaboration, and context switching such that it does not adversely affect the overall performance of the configuration at run-time 3 . Additionally, an application may contain many processes and each process may contain many threads. The ability to capture the characteristic properties of all threads within an application is essential: UML contains an ideal construct for defining goals for entities -Use Cases. UML Use Cases. A UML Use Case is a means of specifying the usage of a system. Use Cases can be structured to represent the usage of each layer within the layered architecture. "The Use Case construct is used to define the behaviour of a system or other semantic entity without revealing the entity's internal structure. Each Use Case specifies a sequence of actions including variants that the entity can perform interacting with actors of the entity." [START_REF]UML 2.0 Specification[END_REF]. An Actor is an entity which is eternal to the system, which interacts with the system, but is not a part of the system. Figure 3

Modelling the Dynamics of an Application

Figure 6 shows a UML Class diagram depicting an application that contains a Process that contains a Thread. The Thread inherits from an Abstract Thread, which exists to manage the three APOS packages (Thread Management, Communications and Synchronisation) from which it constructs its listed interface operations. Further to the static architecture depicted in the Class diagram, Figure 6 also includes the State machine for the Abstract Thread showing how it changes state as a result of calls to the operations defined on its interface. Quality of service characteristics (timing, deadlines etc.) for operations defined on the Abstract Thread Class can be captured within the model. These quality of service properties are inherited by all threads, for example the time to transit from the Dormant state to the Ready state is the same for all threads in the process and is defined only once in the model.

Application Integration

The AL is composed of a set of logical partitions where each partition performs a specific role or set of functions and may be composed of an integration of lower-level processes. For example, one partition may exist to perform utility numerical calculations (e.g. implementing a direction cosine matrix for axis transformations) and another may exist to perform autopilot functions. So as to ensure each partition can be readily re-used this paper explores the idea of wrapping the functional software of each partition into a partition harness. In effect, a partition harness will standardise the provided and required interfaces for each partition and enable each partition to be viewed as a black box i.e. the complexity of any internal software is hidden behind its interface. It must be stressed that this idea is not new; Hatley & Pirbhai [START_REF]Strategies for Real-time System Specifications[END_REF] expounded such a notion back in the late 1980's. Figure 7 shows a UML Structured Class diagram depicting the architecture of a partition harness including three representative processes: There are no restrictions (other than the run-time constraint for the overall partition) on what these processes can and cannot do. They may for example, be concurrently executing threads or alternatively, a serialised processingchain. The Maintenance, Self-Test and Redundancy Management monitor the internal health of the partition. Although the OSL will identify any overrun of hard execution deadlines, the partition may also identify localised errors (constraint errors etc.) that can be captured and handled within the partition. This part of the partition may output diagnostic 4 Although not adopted wholesale amongst IMS practitioners, it is suggested here that SI Units be utilised at this point as it makes the reuse and maintenance of the algorithms within the processes (P1, P2 and P3) far easier.

information to the OSL to facilitate any redeployment of the partition subject to continuous errors being reported. Having said all this, Figure 7 is devoid of any information required to construct a blueprint and serves as an example of the nondomain-specific nature of the UML.

Extending the UML for IMS and the Software Blueprint

Unlike natural languages such as English, which are extended by loan words, semantic changes to existing words and very rarely by new words being added, the UML is a wholly extensible language through a mechanism called stereotyping. A stereotype is applied to a standard UML modelelement to make subtle semantic changes to the standard UML definition of the model-element. Additional properties can be added to the stereotype through what are known as Tag Definitions. When a stereotype is applied to a model-element its Tag Definitions are given values (hence the term Tag Values). In the above example, additional information is required about each instance of the Virtual Channels (Input1 & 2 and Output1 & 2). This includes, for example, how much data is being transferred, the start address of the data, whether the channel is 'on processor' (facilitating communication between two partitions on the same processing element), or 'off processor' (facilitating communication between two partitions on separate processing elements), and any other information required (by the OSL) for monitoring the health of the channel (e.g. corrupt hardware). When we take a look at the partition harness itself, there are also additional properties to be captured for the blueprint. For example, the scheduling period of the partition, the worst-case execution time, and whether the scheduling deadline is a hard (must complete on time) or soft (can overrun) constraint. Yet again, this information about the partition can be captured using a stereotype. Figure 8 shows how Stereotypes and their corresponding Tag Definitions are defined and also how they are applied to the Input1 Port on Figure 7 to complete the capture of information (accessible via the properties editor within ARTiSAN's Real-time Studio): From the information captured in the tag values of the stereotypes it is possible to automatically construct a software blueprint for each partition. Designers of the processes within the application must honour the constraints specified by these tag values during the design process i.e. they act as design constraints.

Hardware Topology and The Hardware Blueprint

The SysML (Systems Modelling Language) was created to enable Systems Engineers to use a standardised notation specifically for their needs. All the model-elements on the following two figures can be stereotyped (as above) to capture the information specific to the hardware topology and summarily extracted from the model to construct the Hardware Blueprint. Because the nodes (N1 to N6) in Figure 9 are typed by the same underlying UML class, they all inherit the same properties. Therefore all the Processing Elements in Figure 5 contain the same decomposition as depicted here in Figure 10. This allows us to define components, and reuse them throughout the system, wherever necessary.

Avionics

possible re-configurations. Not only can the UML be used to construct and maintain an IMS, it can also be used as the basis for the creation and maintenance of a safety case.

Conclusions

For over ten years the initiatives, encompassed today in both ARINC-653 and ASAAC, have been carefully evolving. Other technological advances in hardware, software and in the modelling languages used to document and analyse these types of systems have also evolved. Over 10-years ago, Object Modelling Technique (OMT) [ Ref 10] was used by some to document and analyse these systems. In 1996 OMT was embodied within the UML and its extension, SysML. The SysML and the UML are standardised notations for documenting systems and software. However, far from being languages with fixed semantics, they are extensible, to encompass domain-specific nomenclature.

Although intended as a vehicle for documenting the system under development, it should not be forgotten that information within a model is accessible to many other forms of analysis. An IMS Profile built on the UML and the SysML can capture the specific properties of the system under construction facilitating specialist activities such as performance and schedulability analysis, safety assessment. This is on top of the traditional purpose of the UML and the SysML that being to visualise, conceptualise and document the system under construction. Rather than using many tools to capture design information, all IMS design information can be captured within a single-source repository of a UML model. Given the complexity of interrelationships that exist within a typical IMS, the deployment of the UML for IMS must be interpreted as a positive advantage:

Glossary

Figure 1 :

 1 Figure 1: Federated Architectures

Figure

  Figure1, depicts a number of Line Replaceable Units (LRU's) (e.g. a Radar, an Inertial Navigation Unit (INU)) forming a federated union, typically via a set of communication networks (e.g. MIL-STD-1553B[START_REF]Interface Standard for Digital Time Division Command/Response Multiplex Data Bus[END_REF] data bus) with a central LRU (e.g. a Mission Computer) that manages and coordinates the federated union. Although the majority of avionics systems in service today employ this architecture it is not without its problems. Replacing a LRU is not as simple as its name suggests. Although standards exist for interface specifications for some LRU's (e.g. the SNU-84 Specification for INU data formats), typically suppliers of LRU's enhance the capabilities and therefore extend the

Figure 5 :

 5 Figure 5: Sequence of Interactions based on Use Case (UML Interaction Diagram)

Figure 6 :

 6 Figure 6: Architecture and Dynamics (UML Class and State Diagram)

Figure 7 :

 7 Figure 7: Application Harness (UML Structured Class Diagram) The Input and Output Processing exist to convert the (input) data-stream from the MSL via the OSL into engineering units and then convert them back into the data-stream for output. All the input (Input1 and Input2) and output (Output1 and Output2) ports are typed by the same Virtual Channel class. The Virtual Channel Class is an abstract class that holds only those operations defined within the APOS relevant for that specific channel type. Processes then read information from Input Processing in the correct engineering units 4 . Processes (P1, P2 and P3) represent the functional software within the partition.There are no restrictions (other than the run-time constraint for the overall partition) on what these processes can and cannot do. They may for example, be concurrently executing threads or alternatively, a serialised processingchain. The Maintenance, Self-Test and Redundancy Management monitor the internal health of the partition. Although the OSL will identify any overrun of hard execution deadlines, the partition may also identify localised errors (constraint errors etc.) that can be captured and handled within the partition. This part of the partition may output diagnostic

Figure 8 :

 8 Figure 8: Defining and Applying Stereotypes

Figure 9 :Figure 9 ,

 99 Figure 9: Topology of Processing Elements (SysML Assembly Diagram) Figure 9, a SysML Structured Class Diagram, depicts the overall topology of all hardware nodes within the Avionic System whereas Figure 10 depicts the internal structure of a single hardware node.Because the nodes (N1 to N6) in Figure9are typed by the same underlying UML class, they all inherit the same properties. Therefore all the Processing Elements in Figure5contain the same decomposition as depicted here in Figure10. This allows us to define components, and reuse them throughout the system, wherever necessary.

  depicts capabilities supported by the overall aircraft as Use Cases. At lower levels in the architecture they reveal capabilities commensurate with that level.

							Pilot	Navigator	«Single Press Button»	«Equipment»	«Display Surface»	«Display Surface»	Navigator	VOR ILS	«Singleton»	«Singleton»	«Singleton»
									VOR/ILS	VOR ILS		Head Up (Front)	Head Up (Rear)	«Controller»	«Controller»	TheVORILS
												Format Manager	ILS Manager	:Logical::VOR ILS
												:Formats::Format Manager	:ILS::ILS Manager
							Initiate ILS Landing Sequence
							The Pilot informs the Navigator
							to initiate a landing sequence
							The Navigator selects ILS	Select ILS
							The VOR ILS (Subsystem) receives the request to enter ILS.		Toggle VORILS Mode	{2ms}
							The VOR ILS (Subsystem) informs the VOR ILS (Equipment) to enter ILS mode.	Timeout Required?		Enter ILS {3ms}
							while ILS Not Active loop
							Retrieve the State of the VOR ILS (Equipment) Retrieve the State of the VOR ILS (Equipment)			{1ms} {1ms}	Get State Get State
							end loop
							VOR ILS informs the Format Manager to Display the ILS Format					Activate Format( ILS Format )
							Activate the Head Up (Front) (Display) with the ILS Format					Activate( ILS Format )
							Activate the Head Up (Rear) (Display) with the ILS Format					Activate( ILS Format )
							Activate the ILS Manager					Activate
							while ILS Active loop
							Schedule the ILS Manager Schedule the ILS Manager					Schedule Schedule
		Power Up Warm		«include»	Continuous Built-In Test		Retrieve the Raw Localiser Data Retrieve the Raw Localiser Data Retrieve the Raw Glideslope Data Retrieve the Raw Glideslope Data Retrieve the calculated Localiser position Retrieve the calculated Localiser position					Get Localiser Sym Position Get Localiser Sym Position	Raw Localiser Raw Localiser Raw Glideslope Raw Glideslope
	Power «Primary Actor»	Power Up		Power Up Cold «include»	«include»	Time «Primary Actor»	Retrieve the calculated Glideslope position Retrieve the calculated Glideslope position Update the Head Up (Front) (Display) Update the Head Up (Front) (Display) end loop Update the Head Up (Rear) (Display) Update the Head Up (Rear) (Display)					Update( ILS Symbology ) Update( ILS Symbology ) Update( ILS Symbology ) Update( ILS Symbology )	Get Glideslope Sym Position Get Glideslope Sym Position
				Power Up		Land Aircraft (System Only) Land Aircraft (Software Only) ...
				Built-In Test
						See Store Information Use Case Diagram
				«include»
	«Primary Actor»
	Pilot	Shutdown	«include»	Store Information
				«include»
				Execute
				Mission	«include»
	Communicate
					Load Mission	«Secondary Actor»
						Mission Plan
				See Execute Mission Use Case Diagram
	«Secondary Actor»	«Primary Actor»	«Primary Actor»
	Commander	Navigator		Bombadier
	Figure 3: Aircraft -level Use Cases (UML Use Case
			Diagram)
	High-level Use Cases (such as 'Execute Mission')
	quite obviously require some refinement into lower-
	level Use Cases shown here in Figure 4.
				Pilot
				Execute
				Mission
					«include»
			«include»
	Take Off Aircraft		«include»	Land Aircraft
				Execute Sortie
	Figure 4: Execute Mission (UML Use Case Diagram)
	Use Cases make very few (if any) assumptions
	about underlying architecture and are therefore
	ideally suited to capture 'capabilities'. Yet again
	further refinement is required to elaborate the
	sequence (or invariants) of actions required to
	deliver the 'capability'. It is at this point that the
	logical entities (Applications, Processes etc.) are
	linked together to form a network. This is typically
	done in a Use Case by Use Case manner with the
	underlying model repository managing the overall
	interconnections between the logical entities. UML
	interaction diagrams are used to elaborate the
	behaviour of Use Cases. These include activity
	diagrams, communication diagrams, (formerly called
	collaboration diagrams and renamed in UML 2.0),
	and sequence diagrams. Figure 5 depicts a
	sequence diagram. Properties can be captured for
	each interaction, such as response duration and
	detection lag. Timing budgets for a set of interactions
	can also be documented. This enables a preliminary
	assessment of overall timing requirements for the
	user-level capability.

This should not be read as a failing, standards must be allowed to evolve to encompass technological advances. Standards should be regarded as an expression of the currently accepted state of the art.

The author is acutely aware of this problem having worked on a project where, due to a supplier removing a specific processor from their product range, the hardware had to be changed very late in the project.

It is duly noted here that an application can contain a number of processes and that each process can be multi-threaded. However, the OSL is only interested in scheduling the application; it is left up to the internal scheduling of the application to determine thread execution within given constraints.

Avionics

As well as stereotyping each processing element and its internal components, each link between nodes (and ports) can be stereotyped to capture further quality of service properties relating to bandwidth, speed, protocol, etc. Stereotypes differ from inheritance hierarchies as they can apply to both the class itself as well as the instance. In addition, unique tag values can be specified for each stereotype application. This is especially useful for the Assembly Diagram, where each node (part, port, etc.) will have unique characteristics.

Configuration and Run-time Blueprints

A configuration blueprint links the hardware blueprint with the software blueprint and defines a performance-optimal distribution of partitions amongst the available hardware nodes. Given that all the information required to construct the configuration blueprint now exists within the UML model, it is not beyond the realms of possibility to use this information to assess a set of possible configurations. Taking this to its natural conclusion, assessment can also be made for all possible permutations of configurations and thereby determine the sub-set of all possible configurations that deliver the overall system performance.

Facilitating the Safety Assessment and Audit

Due to the distributed nature of applications and the constraints within which they must conform -coupled with the possibility of a reconfiguration -the safety assessment of an IMS is of paramount importance. Should the algorithm, within the OSL, that determines application deployment derive a suboptimal solution, the whole system may fail as the OSL repeatedly struggles to find the optimal reconfiguration:

We have been discussing static blueprints that capture the performance boundaries within which an individual application must execute (the software blueprint) and the permissible collection of applications that constitute a configuration (the configuration blueprint). Bearing in mind that an IMS can be re-configured at run-time (to cater with failures and/or mission changes), an emulation of this Run-time Blueprint must be created and analysed to assess the suitability of all permutations of re-configurations. It has been suggested [Ref 1] that some form of Genetic Algorithm [Ref 8] be implemented to assess the optimal re-configuration; to date this is work in progress. Given that safety is the responsibility of all project engineers and not just a Safety Assessor, and that properties traditionally unrelated to a safety case are now an integral part of a UML model, a single-source repository of all this information is essential to facilitate a rapid assessment of the required applications within all


Daniel Dollé

Vital software: Formal method and coded processor

Keywords: automatic subways, formal specification, safety critical software, arithmetic coding

Siemens Transportation Systems has been developing mass transit systems for 30 years and for more than 10 years it has used the B formal method to develop and validate its safety critical software. With B, the software is derived stepwise from an abstract mathematical specification and formal proof ensures that each intermediate step is equivalent to the previous one. With the Vital Coded Processor, any run time error caused either by a compiler error or a hardware failure is detected and the unit is set in a safe state. A high level of productivity is achieved through the use of a tool that derives semi-automatically the code from the formal specification.

Introduction

The company

Siemens Transportation Systems is the international expertise centre of Siemens for automated mass transit systems. It is also the supplier in France of the products and services of the "Transportation Systems" group of Siemens AG.

1.2 Urban transit An urban railway system is made of three main parts: the command centre, the car-borne controllers and the zone controllers. The command centre supervises the line and regulates train traffic. It usually has no safety critical mission. The zone controller manages a section of the line: it tracks the trains running on its section and sends them movement authorities that depend on the position of the other trains and the state of the lineside equipment (switches, signals, etc.). The car-borne controllers manage the train's propulsion according to its mission and to the instructions received from the zone controllers. They also open and close the train doors. If platforms are equipped with screen doors, the trains and the zone controllers open and close them collaboratively. The wayside and carborne controllers perform vital functions in software. In order to ensure the very high safety level required for these functions, Siemens Transportation Systems (STS) uses two complementary techniques:

• The B method [START_REF] Abrial | The B-Book[END_REF] is a formal method for the specification, design and coding of software. B ensures that the source code implements the specification without any error. • The Vital Coded Processor [START_REF] Forin | Vital Coded Microprocessor : Principles and Application for various Transit Systems[END_REF] ensures that the executables can cause no harm even in the case of hardware failures or defects in the compiler.

Vital software

The challenge of developing safety critical railway functions in software was met early on with specific technologies.

SACEM: In the '80s, the consortium [START_REF] Hennebert | SACEM : a fault tolerant system for train speed control[END_REF] in charge of building the SACEM (Système d'Aide à la Conduite, à l'Exploitation et à la Maintenance) for the Paris metro authority developed the Vital Coded Processor to protect software execution against hardware and compilation errors. This technique is powerless against design error and classical validation through testing was deemed insufficient. A formal (i.e. mathematical) approach was therefore used.

• The source code (in Modula II) was enriched with pre and postconditions that were then verified semi-automatically. • The specification of the software was rewritten in a formal language. • The consistency of the formal specification and of the annotated code was checked manually. This validation proved to be extremely costly because it had been done after a classical development. For the following Paris automatic subway, Météor, a formal development was required.

Météor: Opened to the public in 1998, Météor [START_REF] Behm | Météor : a Successful Application of B in a Large Project[END_REF] is a driverless system that allows mixed traffic: trains without carborne controllers may run at the same time as equipped trains. Météor was the first application of the B method and it proved remarkably successful: all the errors were found during the development and the validation process was done efficiently without unit tests.

Formal development process

Organisation

The development of safety critical software would classically be organised in a development team, a test team and a safety team. The responsibility of the safety team is to ensure that the software never compromises the safety of the system. The organisation of a formal development is very similar, we simply added a team of formal method specialists in order to provide method and tool support.

Formal support team: The mission of the formal support team is to collect and disseminate best practices.

• It maintains the "B development Guide". This document is a methodological repository where we collect the experience of our formal projects.

Development cycle

The classical development cycle is split into the following phases: specification design, coding and test. The use of B implies some modification, they are detailed below. Software specification: The software is specified in a text document organized along the principles of functional analysis (SADT). The aim of this document is to state clearly and rigorously what the software has to do, it uses whatever notation is best suited to that purpose: natural language, state automata or B formulas. The software specification prepares the formalisation phase, it should identify the following items:

• The data represent the states of the software, the input/output of the functions that specify it or its configuration. • The processing specifies how a function computes its outputs from its inputs and how it modifies its internal states. • The properties are logical assertions that either express safety properties or simply clarify the processing. • The hypotheses are assumptions about the environment of the software. • The limitations give the scope of validity of the data. All those items will later be found in the B model. • The abstract model should not unduly constrain the coding. The means to fulfil these sub-goals are:

• Respect the functional architecture of the software specification. • Divide complex problems into smaller problems that can be treated separately. • Keep the number of B implementations to a minimum. It should be noted that it has a twofold effect. Implementations are poorly readable because they cannot use the concise mathematical notation that is allowed in machines and refinements. Furthermore, since all the implementations are directly translated into code, they have to take into account efficiency constraints. Depending on the complexity of the function to be formalised, a module can be a single machine, a machine and its refinement or a machine, its implementation and one or more machines. In all cases, the machine formalises the part of the requirements that is needed for the outside of the module. For instance: "the speed of the train is lower than a limit".

• If the requirement is simple, it can formalised in a single machine. For instance: "the speed of the train is lower than a limit for the whole line". • If the requirement is more complex, a refinement is added to the machine. For instance: "the speed of the train is lower than one limit on the mainline and lower than another limit in the yard. • If the requirement is still more complex, an implementation is added to the machine. This implementation divides the requirements in smaller requirements that are treated separately. For instance: "the speed of the train is lower than a limit that depends on the slope at the position of the train, the limit can be modified by an operator on work zones". In this case the implementation would divide the problem into two modules that would compute the train position and handle the operator requests. The different items of the textual specification can be found in the abstract model: • The data are the variables and constants.

• The treatments are the operations.

• The properties are either the invariants of B components or the postconditions of operations. • The hypotheses are either modelling choices or postconditions of the operations that interface the formal software with its environment. • The limitations are the preconditions of read operations. Refinement: The goal of the refinement phase is to produce the concrete model. It contains the abstract model as well as the implementation of all the components that were not previously implemented. The following principles apply to this phase: • Except in the case of technical limitations, all the B components should be implemented. • The constraints coming from coding efficiency and memory consumption should be taken into account.

• The difficulty of proof should be kept under control. The refinement brings the abstract model down to code: the sets and relations of the model must be transformed into arrays, the non deterministic constructions of B must be transformed into classical control structure (IF and CASE). If these transformations are carried out simultaneously (each machine or refinement is refined into a single implementation) the resulting proofs can be extremely difficult. The recommended practice is to refine the control structures first and to refine the data later on. Nowadays, the refinement is automated and the developer can concentrate on the new refinement schemes that the tool cannot yet refine and on the run time optimisations. Proof of the B model: The B model is proved at the same time as it is developed. The goal of the activity is to demonstrate that each component is consistent and that it does not contradict the abstraction it refines. The first step of the proof is to compute all the proof obligations foreseen by the B-Book [START_REF] Abrial | The B-Book[END_REF], it is done entirely automatically by the Atelier B. The second step is the actual demonstration of the proof obligations. The Atelier B provides an automatic prover that discharges up to 90 % of the proof obligations. The remainder is proved interactively: the developer can both drive directly the behaviour of the prover and add new proof rules. For the Météor project we added about 1200 proof rules to the internal rule base of the prover. These rules are checked by the validation team in order to ensure integrity of the proof. Compilation: As there is no compiler for B, the implementations must be translated into a classical programming language. In our case this is done entirely automatically and the target language is a subset of Ada. Validation of the vital software: Validating the software consists in ensuring that is execution fulfils the requirements identified in the software specification. The validation of software developed with B goes through the following steps:

• The consistency between the abstract model and the software specification is ensured by functional tests and by an analysis of the model that is carried out by the RAMS team. Ideally, the functional tests should be done early in the development and use only the abstract model. In practice they use the Ada code coming the concrete model.

• The consistency between the abstract and the concrete model is proved. • The consistency between the B implementations and the Ada code is ensured by the use of two diversified translators. An analysis by the RAMS team guarantees that the Ada code of the machines that are not implemented in B is actually a refinement of these machines and it satisfies the requirements. • The consistency between the Ada code and its execution is ensured by the Vital Coded Processor [START_REF] Forin | Vital Coded Microprocessor : Principles and Application for various Transit Systems[END_REF]. Some points worth noticing: As the abstract B model captures all the vital requirements of the software specification, the RAMS team can validate the software without analysing the concrete model. Similarly, all the system-level properties of the model are in its abstract part, the concrete model only contains code-level properties. Since the goal of the tests is to detect modelling errors, the reference for the tests is the software specification and not the abstract model. We have no unit tests, they would check that the code conforms with the detailed design and this is already done by the proof. In the classical life-cycle, the validation is based on testing and can thus only start after the coding. In a B development it starts during the formalisation phase: the developers prove the abstract model before they start refining it. The limits of B: There is no B construct to express explicitly real time constraints. They can nonetheless be modelled under the hypothesis that the software is periodically activated. In our case, the hardware vitally ensures a constant periodicity for software activation. Likewise B has no construct for input/output or for file access. These functions are modelled using a machine that is implemented directly in Ada. A further limitation is that B handles no other numbers than integers. We model real numbers as fixed points and handle the necessary scaling factors explicitly.

Safety techniques

The B method ensures that the implementations comply with the abstract model. It is also necessary to ensure that the software execution complies with the B code. Our technology cannot prevent run time errors but, since our equipments have a safe state (no traction power for a wayside equipment and stopped train for an onboard equipment) we can guarantee that the system will either function correctly or go into a safe state. We use two techniques for that purpose the Vital Coded Processor (VCP) and the redundancy of the B/Ada translation. The Vital Coded Processor: The Vital Coded Processor uses a probabilistic approach to detect inconsistencies between software source code and its execution. Each data of the software has two parts: 32 bits of functional information and N redundant bits. The overall safety level achieved depends on N but not on the technology used. It is, for instance, independent of the hardware reliability and no validation of the compilation tools is necessary. The redundant part is the sum of three terms:

• An arithmetic encoding of the functional value detects data alteration in memory or during their copy. • A signature detects instructions executed in an incorrect sequence. As this signature is static, independent of the functional information, it can be pre-computed off-line. • A time-stamp for each computation cycle ensures that the previous value of a variable cannot be used after an update. After giving a signature to each input variable, the Signature Predetermination Tool (SPT) analyses the source code and computes the expected signatures for the output variables. These pre-computed signatures are then embedded in the executable. A run time, the data are computed using a library of elementary operations (arithmetic, test condition computation, loops, etc.) that updates both the information and redundant parts. At the end of each computing cycle, a failsafe hardware component called the dynamical controller compares the actual value of the signatures with their actual value. In case of discrepancy, the dynamical controller puts the equipment in a safe state. For efficiency reasons, this comparison is not done for each variable but for a single variable that is built to have the property that it "collects" every error: as long as the computation cycle is less than 2 N operations, an error in any variable is detected with a probability 1 -2 -N . As in our implementation of the VPC 2 N is roughly equal to 10 14 , for all practical purpose we are certain to detect any error. The safety provided by the VPC relies on the diversity of the source code analysis done by the compiler and the SPT. We assume that there is no common failure mode because they have been developed independently (different teams and languages). B/Ada translation: The VPC ensures that the software runs correctly with respect to its source code. It is also necessary to guarantee that the source code is correct with respect to the B implementation that it translates. We use two translators for that purpose: they have been developed fully redundantly (teams, design and programming language were different) on a common specification.

Figure 2: Translating B to Ada

As shown in figure 2, we use the VPC to compare Ada source codes: one set of source files is compiled and the other is analysed by the SPT. Any error (in the translator, the compiler, the linker or at run time) will result in a difference between the precomputed signatures and the signatures and their run-time value.

Tools for the B method

Commercial tools: Atelier B

The core tool for formal development at Siemens Transportation Systems is the Atelier B. This product, developed and marketed by ClearSy [5], supports all the features needed to manage an industrial-scale formal development and to rigorously apply the B method.

• The model can be structured and teamwork is supported. In our case, the typical size of our applications is: five hundred files, a few hundred thousands line of B model, a few tens of thousands of proof obligations, 10 to 15 submodels, formal development teams of up to 10 persons. 3.2 Proprietary tools: EdithB STS has developed many tools that enhance the efficiency of formal development, the most significant is an automatic refiner called EdithB. The problem: A typical beginner's mistake is to implement simultaneously an abstract variable and the operations on this variable. This results in complex proof because abstract processing on abstract variables must be checked against concrete processing on concrete variables. An experienced B developer will proceed differently:

• Intermediate implementations are used to refine the operation one step at a time. • Variables are refined last.

The resulting architecture looks like: In such an architecture the variables of A 0 , ..., A n are abstract. It is only in A_imp n that the variables are implemented. Similarly, each operation Op i of A i is implemented in A_imp i with a sequence of operations call to operations in A i+1 : Op i1 , ..., Op im . Since each of the new operations Op ij only uses abstract data, it easy to prove that they refine Op i . A drawback of this technique is that it is very repetitive: each new machine repeats piecewise information that was present in the previous machine. Météor: One of the key results of the Météor project was the identification of a very small number (less than 10) of standard data refinement schemes. Using a small number of refinement schemes led to a great uniformity of coding style that eased the review process and reduced the number of proof rules that had to be written (a proof rule useful for a given use of the refinement scheme was likely to be reusable for another instance of this refinement scheme). The solution: These refinement schemes were first collected in a "B Method Guide" and used during the development and review process of our models. Later, they were implemented as rewriting rules in our automatic refinement tool. The tool takes as input an abstract B component (a machine or a refinement) and produces an implementation of this component. As this implementation may import a new machine, the process is iterated until a terminal implementation is produced. Principles: EdithB is made of two parts: a rule base and an interpreter for this rule base. The interpreter is a stable software that has not changed much since its creation in 1999. The rule base is dedicated to our applications: it can only refine the B constructs that we use. It is a growing body that has been enriched in the course of our successive formal developments. The result is that, even though we may not always be reusing code directly, we are reusing the expertise that went into its writing. An example: The rule base can be divided into two parts: rules for the refinement of variables and rules for the refinement of instructions. Their respective behaviour will be explained with an example.

• To refine an abstract variable one has to define the concrete variable that implements it and how both are related (the "gluing" invariant). A simplified example of variable refinement rule is shown below.

RULE set_variable IS

ABSTRACT_VARIABLE a TYPE integer_set(a,n) INVARIANT a ⊂ 1..n CONCRETE_VARIABLE Machine A 0 Implementation A_imp 0 Machine A 1 Implementation A_imp 1 Machine A n Implementation A_imp n IMPORTS a_r INVARIANT a_r ∈ 1..n → BOOLEAN & a = a_r -1 [{TRUE}] END
The abstract variable "a" is a set of integers, it is implemented with an array of booleans called "a_r" and the gluing is that "a" is exactly the set of indexes for which "a_r" is TRUE. A theoretical limit of our tool is that it chooses the refinement of a variable without taking into account how this variable is used. As a consequence, it chooses the most general refinement, the one that works for every conceivable use of the variable. In the example above, if only the maximum of "a" is ever accessed, it is more efficient to refine "a" with a_max = max(a). In our experience, this limit is not significant. This rules copies b into a local variable and then updates the array that refines the set. As the second statement need not be refined further, it is marked as an implementation. The first statement is not marked, so it could be refined further. This could useful be useful if b were instantiated with a complex expression but in our case b is just "my_var", so the resulting expression would simply be: l_1 := my_var; my_set_r(l_1) := TRUE;

Interactive refinement: The automatic refiner has an interactive mode where the context and applicable rules of each refinement step can be examined. This mode is used in two situations.

• EdithB can fail to find any rule matching the current context. • The refined code is incorrect or not efficient enough. In both cases, the developer debugs the refinement in interactive mode and writes the rules that give the desired refinement. These rules can then be stored for use on the current B machine or, more rarely, they can be added to the rule base if they are deemed reusable. Validation of EdithB: Since the B components it produces are proved, no safety validation is needed for the refiner. EdithB in use: When we built EdithB in 1999, we compared its output to the manually written code of a previous formal project. There was a small increase in code size but no significant effect on computation time. The expected savings in development time led us to generalise it for all of our formal software since that time. It is now a fundamental part of our software development process. The following diagram shows the proportion of automatically generated B code for a project that is currently nearing completion (the scale is in kilo-lines of uncommented B).

Conclusion

This paper has given a short overview of the development of safety critical software at STS. The technical heart of our process is the B method and the Vital Coded Processor. A highly automated development process defined around B allows us to build error-free source code in a cost efficient way. The VCP ensures that this source code runs safely on the computer platform without any safety requirement on the CPU. We can thus guarantee rigorously that no defect is introduced between the formal specification of the software and its execution. The whole process is the result of two decades of progressive improvements. It is fully consistent with the requirement for vital functions inside an industrial/product organisation.

Glossary

Figure 1 :

 1 Figure 1: Comparison of the classical and formal development cycle Formalisation: The goal of the formalisation is to express in B the content of the software specification. This phases ends when all the requirements have been captured in the abstract model. Ideally, it can then be refined without knowing the textual software specification. The development of the abstract model is constrained by technical sub-goals: • Checking the compliance of the formal model with respect to the software specification should be easy. • The proof should be easy.

Figure 4 :

 4 Figure 4: A typical refinement architecture

Figure 5 :

 5 Figure 5: Number of refinement rules

Figure 6 :

 6 Figure 6: Canarsie Line carborne controller Since only the implementations are translated into Ada code, around 2/3 of this provably correct application is produced automatically.

•

  It provides tool and method support to the developers and ensures by means of technical reviews that the B models are provable and efficient.• It may participate in critical parts of the development and coach new developers. As most of our team now have experienced B developers, the role of the formal development team is becoming less crucial.

		• It checks the Ada code of the parts of the
		application that are not developed formally.
		• It validates the interactive proofs.
		• It specifies and implements its own tests of the
		vital requirements.
		These activities may result in problem reports that
		have to be corrected by the development team.
		2.2 An overview of the B language
		B is a formal language invented by Jean-Raymond
		Abrial. Close to other formal language such as Z and
		VDM, B covers the full development cycle and is
		suitable for large scale developments. Is main
		characteristics are:
		• B has a mathematical basis that is both powerful
		and easy to learn: elementary set theory and
		ordinary two-valued predicate logic.
		• Proofs are at the heart of B: every property that
		is expressed in a B model must be proved.
		• B gives the developer a uniform view of the
		formal specification and its code: the same
		notation is used for both.
		• The B model is made of modules that provide
		data and operations on these data. A module is
		further divided into: a Machine, a Refinement
		and an Implementation. The machine gives the
	Development team: The development team carries	external view of the module: it shows only what
	out all the activities going from the writing of the	is needed by users of the module. The
	software specification to the software target	refinement gives the internal view of the module:
	integration.	it specifies completely the behaviour of the
	• It writes the software specifications. • It formalises the specification in an abstract model. • It refines the abstract model in order to obtain	module. Machines and refinements are abstract components: a data can be a set or a relation. An implementation, on the other hand, is concrete: it is directly translatable into a classical language and its data structures are very limited
	code that can be translated into a classical	(integer, booleans and arrays).
	programming language. • It proves all the proof obligations required by the	• B is fully supported by a tool: the "Atelier B" [5].
	B method.
	• It produces the Ada code of the software. This
	code is either automatically translated from B
	implementations or manually written for the low-
	level input/output primitives of the application.
	Test team: The test team defines and implements
	the tests that software must pass.
	Validation team: The validation team is independent
	of the other teams and analyses each of the
	intermediate productions of the development team.
	Its goal is to identify early any defect that could lead
	to a dangerous situation.
	• It validates the software specification.
	• It checks that all the vital requirements of the
	software specification are captured in the
	abstract model.

  • The features available for the B method are: static checks of the B files (syntax and type checks, visibility rule checks, etc.), proof

	obligation generation, automatic and interactive
	proof, translation of the B implementations into
	Ada.
	B
	implementations
	Translator 1	Translator 2
	Ada code 1	Ada code 2
	SPT	Compiler
	Reference	Object code
	signatures
		Linker
	Executable

•

  The rules that refine instructions work within a context defined by the variable refinements and by the hypotheses that are at the point of refinement. Let us suppose we wish to refine the assignment to "my_set" that is inside the IF:

	INVARIANT
	my_set ⊂ 1..99
	OPERATIONS
	my_operations =
	IF 3 ∈ my_set THEN
	my_set := my_set ∪ {my_var}
	END
	The context available to an instruction
	refinement rule contains: integer_set(my_set,99)
	(coming from the variable refinement rule we
	saw previously) and 3 ∈ my_set.
	• With this context the following rule would apply:
	RULE assign_set_variable IS
	WHEN integer_set(a,n)
	REFINE
	a := a ∪ {b}
	INTO
	local_variable_1 := b;
	IMPLEMENTATION(
	a_r(local_variable_1) := TRUE)
	END

  CBTC Communications Based Train Control EdithB Automatic refinement tool RAMS Reliability Availability Maintainability and Safety STS Siemens Transportation Systems VCP Vital Coded Processor