https://www.mdu.se/

In some domains, standards such as ISO 26262 or the UK Ministry of DefenceÂ’s Defence Standard 00-56 require developers to produce a safety case. As the safety case for a complex system can be rather large, automated verification of all or part of it would be valuable. We have approached the issue by designing a method supported by a framework including analysers for safety cases defined in the Goal Structuring Notation (GSN) and systems modelled in the Architecture Analysis and Design Language (AADL). In our approach, the safety case predicates are defined in a subset of the functional language Meta Language (ML). Our approach facilities formalising some parts of a typical safety argument in an ML-like notation, enabling automatic verification of some reasoning steps in the safety argument. Automatic verification not only justifies increased confidence, it can ease the burden of re-checking the safety argument as it (and the system) change.

For a large and complex safety-critical system, where safety is ensured by a strict control over many properties, the safety information is structured into a safety case. As a small change to the system design may potentially affect a large section of the safety argumentation, a systematic method for evaluating the impact of system changes on the safety argumentation would be valuable. We have chosen two of the most common notations: the Goal Structuring Notation (GSN) for the safety argumentation and the Architecture Analysis and Design Language (AADL) for the system architecture model. In this paper, we address the problem of impact analysis by introducing the GSN and AADL Graph Evaluation (GAGE) method that maps safety argumentation structure against system architecture, which is also a prerequisite for successful composition of modular safety cases. In order to validate the method, we have implemented the GAGE tool that supports the mapping between the GSN and AADL notations and highlight changes in impact on the argumentation. © 2012 IEEE.

Embedded systems are ubiquitous in the modern world. They are microcomputers most often included incomplete devices consisting of software and hardware. Embedded systems range from small devices to large systems monitoring and controlling complex processes. Design and development of such systems is a complex task, since embedded systems often need to fulfill extra-functional requirements, on top of functional ones, within constrained amounts of platform resources. Some embedded systems are mission critical; hence, they are not allowed to fail during the mission. One way to ensure that a system works in accordance to its specification is to define the system in an Architecture Description Language (ADL) and apply formal verification methods. The Architecture Design and Analysis Language (AADL) has become popular in the avionic and automobile industry, and is equipped with several annexes, among them the Behavior Annex. However, AADL still misses a formal semantics, which prevents the possibility to prove correctness of architecture features by performing model checking on AADL models. Moreover, AADL does not support time annotations, which prevents modeling of real-time systems in AADL.

In this thesis, we address these issues by presenting a formal analysis framework including a denotationalsemantics for a subset of the AADL and its Behavior Annex, which evaluates properties defined in Computation Tree Logic (CTL) by providing model checking. Model checking is a formal verification method that has proved to be powerful as well as effective. Our AADL-semantics is supported by a tool with an implementation of the semantics in Standard ML, which in turn is encapsulated in an Eclipse plugin.We also present a time annotation extension of AADL, implemented in a tool translating time annotated AADL and its Behavior Annex into the Timed Abstract State Machine (TASM) for simulation of real-time features. Another closely related problem is how to achieve optimal component distribution; in order to address this issue we have developed a tool that perform near-optional component distribution in regard to a series of parameters.

The research results, which have been validated thought case studies, provides the possibility for a system engineer to model a system and prove its correctness. The research has been conducted in the context of the PROGRESS research center, for predictable embedded software systems.

As system failure of mission-critical embedded systems may result in serious consequences, the development process should include verification techniques already at the architectural design stage, in order to provide evidence that the architecture fulfils its requirements. The Architecture Analysis and Design Language (AADL) is a language designed for modeling embedded systems, and its Behavior Annex defines the behavior of the system. However, even though it is an internationally used industry standard, AADL still lacks a formal semantics and is not executable, which limits the possibility to perform formal verification. In this paper, we introduce a formal analysis framework for a subset of AADL and its Behavior Annex, which includes the following: a denotational semantics, its implementation in Standard ML, and a graphical Eclipse-based tool encapsulating the implementation. We also show how to perform model checking of AADL properties defined in the Computation Tree Logic (CTL).

We present a denotational semantics for the Architecture Analysis and Design Language with Behavior Annex and the Computational Tree logic. We also present tool support as an OSATE plug-in as well as the Production Cell case study.

Due to the growing complexity of software systems in modern automo- biles, the software architecture design phase becomes more and more important. Useful tools and languages are speci¯cally needed to man- age this complexity. Recently, the Architecture Analysis and Design Language (AADL) has been proposed as a modeling language for crit- ical systems and this language is becoming increasingly popular in the automobile industry. In order to test whether AADL is suitable for modeling software in automobile systems, we provide in this technical report a critical evaluation of the capabilities and features of this new language. Speci¯cally, we evaluate AADL against a set of requirements that have been identi¯ed based on an exhaustive literature review and experiences gained from modeling an Adaptive Cruise Control (ACC) in AADL. The objective of this paper is to evaluate the suitability of AADL and identify gaps that would require future research and devel- opment.

The Architecture Analysis and Design Language (AADL) is a popular language for architectural modeling and analysis of software intensive systems in application domains such as automotive, avionics, railway and medical systems. These systems often have stringent real-time requirements. This paper presents an extension to AADL's behavior model using time annotations in order to improve the evaluation of timing properties in AADL. The translational semantics of this extension is based on mappings to the Timed Abstract State Machines (TASM) language. As a result, timing analysis with timed simulation or timed model checking is possible. The translation is supported by art Eclipse-based plug-in and the approach is validated with a case study of an industrial production cell system.

An Architecture Description Language (ADL) can be described as a language designed to model a system at an architectural level with respect to its software, hardware, and communication links. Due to the increasing complexity of software systems in areas like embedded control and web-based information systems, modelling with ADLs have gained attention in the research community and in practical software development projects. The specific aim of this technical report is to provide a literature review on ADLs for automotive software systems. This literature review consequently focuses on aspects that are relevant for automotive systems like safety, reliability and modelling of Electronic Control Units (ECU).