From Rigorous Requirements Engineering to Formal System Design of Safety-Critical Systemsby Christophe Ponsard, Philippe Massonet, Gautier Dallons The majority of systems that control our daily lives rely on software. Often this software is embedded in the device and remains invisible to users. While the consequences of a failure may be minor, such as failing to deliver part of the requested service, they may also be dramatic, possibly causing human injury or even fatalities (eg car crashes or train collisions). In recent years, CETIC (Centre d'Excellence en Technologies de l'Information et de la Communication) has devoted significant effort to the development of industrial methods and tools that target safety-critical software, with a specific focus on the early phase of system development. At this level, the consequences of design flaws are the most dramatic and costly to correct. Large studies like Chaos (Standish Group) have also shown that these flaws remain the principal reason for project failure. To improve this, the following topics, illustrated in Figure 1 using the V reference model, are being investigated from a model-driven engineering perspective.  Figure 1: Scope in the V-model. At the start of the life cycle, rigorous engineering of requirements aims to provide adequate methods and tools to capture, formalize and perform early verification and validation of critical requirements. Immediately following this, a strong connection with industrial development methodologies is required. Good candidates are Event-B/B (a generic proof-oriented formal language) and AADL (architecture description language). At the other end of the life cycle, the certification process should support adequate techniques for a high level of assurance. Rigorous Requirements Engineering
Providing Connections with Industrial Development First, the FP7 DEPLOY (industrial deployment of system engineering methods providing high dependability and productivity) project aims at the industrial deployment of the Event-B method, a system-level variant of the B method. This method is quite generic and is being applied in sectors such as automotive, train, space and even e-business. Like B, it is mainly proof-based. It is supported by the RODIN (Rigorous Open Development Environment for Complex Systems) proof environment which is Eclipse-based and includes plug-ins for model-checking (ProB) and animation. Bridging the gap between requirements and Event-B models has been identified as a major topic. Second, the ITEA2 SPICES (on Support for Predictable Integration of mission Critical Embedded Systems) project is domain-specific: it targets embedded systems and relies on a formal architectural description language called AADL. Verifications are oriented towards real-time properties and resources management. The connection with requirements models is currently developed both for the structural and dynamic parts of AADL, as shown in Figure 2. Again, Eclipse-based tools are available (TOPCASED).  Figure 2: Requirements (KAOS) to AADL mapping. Supporting Certification at High Assurances Levels Higher assurance levels require a more formal demonstration of correctness. Formal models, which support the rigorous development of the system, can also directly support the certification process. This means not only that the effort required for certification is not increased for such systems, but that the perception of the certification process is also improved, since it is seen as being better integrated with the system products and not as additional work. Our current work mainly targets the aeronautics domain. Links: Please contact: |
cetic.be