Publications for students
Students are required to read and present a paper (proposed by the professors, or proposed by the student and agreed by the professors) related to the topic of the course.
The list of papers proposed by the professors can be found below. The chosen publication can be asked from the professors or via email to ahorvath@mit.bme.hu.
| 1. |
Frank Ortmeier, Gerhard Schellhorn: Formal Fault Tree Analysis - Practical Experiences
|
|
Abstract:
Safety is an important requirement for many modern systems. To ensure safety of complex critical systems, well-known safety analysis methods have been formalized. This holds in particular for automation sytsems and transportation systems. In this paper we present the formalization of one of the most wide spread safety analysis methods: fault tree analysis (FTA). Formal FTA allows to rigorously reason about completeness of a faulty tree. This means it is possible to prove whether a certain combination of component failures is critical for system failure or not. This is a big step forward as informal reasoning on cause-consequence relations is very error-prone.
We report on our experiences with a real world case study from the domain of railroads. The here presented case study is – to our knowledge – the first complete formal fault tree analysis for an infinite state system. Until now only finite state systems have been analyzed with formal FTA by using model checking.
|
|
| 2. |
Tony Rosqvist, Risto Tuominen: Qualification of Formal Safety Assessment: an exploratory study |
| Abstract: Formal Safety Assessment (FSA) is an approach adopted by the International Maritime Organisation (IMO) to support a systemic and structured assessment of proposals for new international regulations to improve shipping safety. Several case studies based on the approach have been conducted during recent years. This paper addresses the issue of confidence in a FSA, as encountered during three case studies conducted by the authors over the years 1998–2002. A peer review process—FSA qualification—is introduced to support the consolidation of confidence in FSA results. Some qualification criteria are suggested. | |
| 3. |
Wan-Hui Tseng, Chin-Feng Fan: Systematic scenario test case generation for nuclear safety systems |
Abstract:
ContextThe current validation tests for nuclear software are routinely performed by random testing, which leads to uncertain test coverage. Moreover, validation tests should directly verify the system’s compliance with the original user’s needs. Unlike current model-based testing methods, which are generally based on requirements or design models, the proposed model is derived from the original user’s needs in text through domain-specific ontology, and then used to generate validation tests systematically. ObjectiveOur first goal is to develop an objective, repeatable, and efficient systematic validation test scheme that is effective for large systems, with analyzable test coverage. Our second goal is to provide a new model-based validation testing method that reflects the user’s original safety needs. MethodA model-based scenario test case generation for nuclear digital safety systems was designed. This was achieved by converting the scenarios described in natural language in a Safety Analysis Report (SAR) prepared by the power company for licensing review, to Unified Modeling Language (UML) sequence diagrams based on a proposed ontology of a related regulatory standard. Next, we extracted the initial environmental parameters and the described operational sequences. We then performed variations on these data to systematically generate a sufficient number of scenario test cases. ResultsTest coverage criteria, which are the equivalence partition coverage of initial environment, the condition coverage, the action coverage and the scenario coverage, were met using our method. ConclusionThe proposed model-based scenario testing can provide improved testing coverage than random testing. A test suite based on user needs can be provided. |
|
| 4. |
Christian Raspotnig, Andreas Opdahl: Comparing risk identification techniques for safety and security requirements |
| Abstract: When developing systems where safety and security are important aspects, these aspects have to be given special attention throughout the development, in particular in the requirements phase. There are many similar techniques within the safety and security fields, but few comparisons about what lessons that could be learnt and benefits to be gained. In this paper different techniques for identifying risk, hazard and threat of computer-supported systems are compared. This is done by assessing the techniques’ ability to identify different risks in computer-supported systems in the environment where they operate. The purpose of this paper is therefore to investigate whether and how the techniques can mutually strengthen each other. The result aids practitioners in the selection and combination of techniques and researchers in focusing on gaps between the two fields. Among other things, the findings suggest that many safety techniques enforce a creative and systematic process by applying guide-words and structuring the results in worksheets, while security techniques tend to integrate system models with security models. | |
| 5. | Mirko Jakovljevic, Astrit Ademaj: Distributed IMA: Use cases for embedded platforms |
|
Abstract:
Distributed IMA, as described in RTCA DO-297, has been used in different forms since 1980s in avionics and modular aircraft control architectures which deploy synchronous or time-division multiplexing for deterministic communication. Such a time-driven communication enables specific capabilities in architecture and embedded platform design, which cannot be realized by asynchronous communication. In complex integrated systems, Distributed IMA enables full virtualization of embedded resources to host distributed hard RT functions. Distributed IMA supports full separation of controlled objects (actuators), input/output devices and sensors from the computing modules in aerospace and other cross-industry applications. This simplifies reconfiguration, and design of generic open architectures. With synchronous and time-division multiplexing in Ethernet networks, critical functions can also be hosted in open systems or in systems where the behavior of non-critical functions cannot be fully assessed.
|
|
| 6. |
Kateryna Netkachova, Kevin Müller, Michael Paulitsch, Robin Bloomfield: Investigation into a layered approach to architecting security-informed safety cases |
| Abstract: The paper describes a layered approach to analysing safety and security in a structured way and creating a security-informed safety case. The approach is applied to a case study - a Security Gateway controlling data flow between two different security domains implemented with a separation kernel based operating system in an avionics environment. We discuss some findings from the case study, show how the approach identifies and ameliorates important interactions between safety and security and supports the development of complex assurance case structures. | |
| 7. |
Josh Newell, Linna Pang, David Tremaine, Alan Wassyng, Mark Lawford: Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application |
| Abstract: The trip computers for the two reactor shutdown systems of the Ontario Power Generation (OPG) Darlington Nuclear Power Generating Station are being refurbished due to hardware obsolescence. For one of the systems, the general purpose computer originally used is being replaced by a programmable logic controller (PLC). The trip computer application software has been rewritten using function block diagrams (FBDs), a commonly used PLC programming language defined in the IEC 61131-3 standard. The replacement project’s quality assurance program requires that formal verification be performed to compare the FBDs against a formal software requirements specification written using tabular expressions (TEs). The PVS theorem proving tool is used in formal verification. Custom tools developed for OPG are used to translate TEs and FBDs into PVS code. In this paper, we present a method to rigorously translate the graphical FBD language to a mathematical model in PVS using an abstract syntax to represent the FBD constructs. We use an example from the replacement project to demonstrate the use of the model to translate a FBD module into a PVS specification. We then extend that example to demonstrate the method’s applicability to a Simulink-based design. | |
| 8. |
Matthew John Squair: Issues in the Application of Software Safety Standards |
|
Abstract:
The application of software safety standards as part of the development of safety critical software is usually considered an essential element of any safety program. Yet it is fairly rare for safety practitioners to step back and critically evaluate both the effectiveness and limitations of such standards. Naive implementations of safety standards can lead to over reliance on weak inductive arguments as to the safety of the software. Whilst incorrect requirements have been identified as a major cause of software accidents it appears that current software safety standards do not place a proportionate emphasis upon this causal factor. Additionally focusing upon the definition of process as opposed to the documentation of lessons learned the majority of software safety standards also appear inadequate to serve as repositories of the ‘state of the art’. This paper examines the limitations, practical problems and issues associated with the use of current software safety standards. The evolution of software safety standards is reviewed and contrasted to the safety standards of other engineering disciplines. The paper then goes onto discuss problems with the current process based software safety standards and considers whether these standards in fact address the real causes of software related accidents. Finally the often overlooked pragmatic issues of applying safety standards are discussed. Due to space considerations the primary standards discussed are DEF-STAN 00-55 and 00-56, MIL-STD-882C, ARP 4761, ARP 4754, IEC 61508, DEF AUST 5679 and RTCA/DO-178B1. |
|
| 9. |
Risto Nevalainen, Juha Halminen, Hannu Harju, Mika Johansson: Certification of software in safety-critical I&C systems of nuclear power plants |
|
Abstract:
Nuclear power plants have well-defined processes to acquire and qualify safety-critical systems. Ultimate goal is to maximise safety, without compromises in quality and reliability. Each new device and system in nuclear power plant shall be classified and qualified according to its safety requirements. Using modern technology means in practice that more and more components have programmable features. The reliability of such components has proven to be difficult to demonstrate due to the nature of flaws in software. Conformance with standards is not any absolute guarantee for safety. It can be achieved only by use of several different approaches, which all provide their own evidences and support for qualification and licensing. Certification is one way to package different methods together and build trust in achievement of maximal safety. In fact, certification is already de-facto “must” in highest safety category of software intensive safety-critical systems. Certification should be aligned with system acquisition, development and commissioning processes to improve total effectiveness of qualification. Then it is also cost-effective and proactive rather than additional and isolated activity. As a part of Finnish nuclear research program SAFIR2010, a project called CERFAS has defined necessary software certification services for nuclear industry needs. Main areas of the service are process assessment and product evaluation. Certification employs also several other method families, like inspections and reviews, independent V&V, model checking, conformance with selected reference standard(s) and use of selected measurements and analyses. Safety case is the main framework to integrate all methods together. |
|
| 10. |
Simon Burton, Jürgen Likkei, Priyamvadha Vembar, Marko Wolf: |
| Abstract: Standard approaches to functional safety as described in the automotive functional safety standard ISO 26262 are focused on reducing the risk of hazards due to random hardware faults or systematic failures during design (e.g. software bugs). However, as vehicle systems become increasingly complex and ever more connected to the internet of things, a third source of hazard must be considered, that of intentional manipulation of the electrical/electronic control systems either via direct physical contact or via the systems’ open interfaces. This article describes how the process prescribed by the ISO 26262 can be extended with methods from the domain of embedded security to protect the systems against this third source of hazard. | |
| 11. |
Dean C. Wardell, Robert F. Mills, Gilbert L. Peterson, Mark E. Oxley: A Method for Revealing and Addressing Security Vulnerabilities in Cyber-Physical Systems by Modeling Malicious Agent Interactions with Formal Verification |
| Abstract: Several cyber-attacks on the cyber-physical systems (CPS) that monitor and control critical infrastructure were publically announced over the last few years. Almost without exception, the proposed security solutions focus on preventing unauthorized access to the industrial control systems (ICS) at various levels – the defense in depth approach. While useful, it does not address the problem of making the systems more capable of responding to the malicious actions of an attacker once they have gained access to the system. The first step in making an ICS more resilient to an attacker is identifying the cyber security vulnerabilities the attacker can use during system design. This paper presents a method that reveals cyber security vulnerabilities in ICS through the formal modeling of the system and malicious agents. The inclusion of the malicious agent in the analysis of an existing systems identifies security vulnerabilities that are missed in traditional functional model checking. | |
| 12. |
P. Cuenot, C. Ainhauser, N. Adler, S. Otten, F. Meurville: Applying Model Based Techniques for Early Safety Evaluation of an Automotive Architecture in Compliance with the ISO 26262 Standard |
|
Abstract: In 2011, the automotive industry introduced the application of a standardized process for functional safety-related development of automotive electronic products. The related international standard, ISO 26262 functional safety for road vehicles, has high demands on process documentation and analysis. Within an engineering context this challenges the tremendous increase of complexity for modern automotive systems and high productivity demands for industrial competiveness purpose. Model based development techniques based on an Architecture Description Language (ADL) has been identified as the best candidate to manage the system complexity and the related safety analysis with the benefit of formal description and capabilities for test automation. The proposed concept relies on the definition of a compositional error modeling approach tightly coupled with the system architecture model, capable to analyze the software and hardware architectures and implementations. This paper explains the results of the language extension based on the EAST-ADL and AUTOSAR domain model in terms of early safety evaluation of an automotive architecture, automating the qualitative and quantitative assessment of road vehicle products as claimed by the application of the ISO 26262. |
|
| 13. |
John Birch, Roger Rivett, Ibrahim Habli, Ben Bradshaw, John Botham, Dave Higham, Peter Jesty, Helen Monkhouse, Robert Palin: Safety Cases and their role in ISO 26262 Functional Safety Assessment |
|
Abstract: Compliance with the automotive standard ISO 26262 requires the development of a safety case for electrical and/or electronic (E/E) systems whose malfunction has the potential to lead to an unreasonable level of risk. In order to justify freedom from unreasonable risk, a safety argument should be developed in which the safety requirements are shown to be complete and satisfied by the evidence generated from the ISO 26262 work products. However, the standard does not provide practical guidelines for how it should be developed and reviewed. More importantly, the standard does not describe how the safety argument should be evaluated in the functional safety assessment process. In this paper, we categorise and analyse the main argument structures required of a safety case and specify the relationships that exist between these structures. Particular emphasis is placed on the importance of the product-based safety rationale within the argument and the role this rationale should play in assessing functional safety. The approach is evaluated in an industrial case study. The paper concludes with a discussion of the potential benefits and challenges of structured safety arguments for evaluating the rationale, assumptions and evidence put forward when claiming compliance with ISO 26262. |
|
| 14. |
Christoph Schmittner, Thomas Gruber, Peter Puschner, Erwin Schoitsch: Security Application of Failure Mode and Effect Analysis (FMEA) |
| Abstract: Increasingly complex systems lead to an interweaving of security, safety, availability and reliability concerns. Most dependability analysis techniques do not include security aspects. In order to include security, a holistic risk model for systems is needed. In our novel approach, the basic failure cause, failure mode and failure effect model known from FMEA is used as a template for a vulnerability cause-effect chain, and an FMEA analysis technique extended with security is presented. This represents a unified model for safety and security cause-effect analysis. As an example the technique is then applied to a distributed industrial measurement system. | |
| 15. |
Alexandre Albore, Silvano Dal Zilio, Marie De Roquemaurel, Christel Seguin, Pierre Virelizier: Timed Formal Model and Verification of Satellite FDIR in Early Design Phase |
| Abstract: In a previous work, we proposed an extension of the AltaRica language and tools to deal with the modelling and analysis of failures propagation in presence of timed and temporal constraints. This need is crucial in the space industry, where safety functionalities raise new challenges for the early validation of systems during model conception. This paper focuses on the application of our approach to the Failure Detection Isolation and Recovery (FDIR) mechanisms of the Attitude and Orbit Control System (AOCS) of a satellite. We discuss the modelling methodology applied to this system and its properties, as well as the tractability of the model-checking analysis. |
