| 1. |
- Cai, Simin
(författare)
-
Systematic Design of Data Management for Real-Time Data-Intensive Applications
- 2017
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Modern real-time data-intensive systems generate large amounts of data that are processed using complex data-related computations such as data aggregation. In order to maintain the consistency of data, such computations must be both logically correct (producing correct and consistent results) and temporally correct (completing before specified deadlines). One solution to ensure logical and temporal correctness is to model these computations as transactions and manage them using a Real-Time Database Management System (RTDBMS). Ideally, depending on the particular system, the transactions are customized with the desired logical and temporal correctness properties, which are achieved by the customized RTDBMS with appropriate run-time mechanisms. However, developing such a data management solution with provided guarantees is not easy, partly due to inadequate support for systematic analysis during the design. Firstly, designers do not have means to identify the characteristics of the computations, especially data aggregation, and to reason about their implications. Design flaws might not be discovered, and thus they may be propagated to the implementation. Secondly, trade-off analysis of conflicting properties, such as conflicts between transaction isolation and temporal correctness, is mainly performed ad-hoc, which increases the risk of unpredictable behavior.In this thesis, we propose a systematic approach to develop transaction-based data management with data aggregation support for real-time systems. Our approach includes the following contributions: (i) a taxonomy of data aggregation, (ii) a process for customizing transaction models and RTDBMS, and (iii) a pattern-based method of modeling transactions in the timed automata framework, which we show how to verify with respect to transaction isolation and temporal correctness. Our proposed taxonomy of data aggregation processes helps in identifying their common and variable characteristics, based on which their implications can be reasoned about. Our proposed process allows designers to derive transaction models with desired properties for the data-related computations from system requirements, and decide the appropriate run-time mechanisms for the customized RTDBMS to achieve the desired properties. To perform systematic trade-off analysis between transaction isolation and temporal correctness specifically, we propose a method to create formal models of transactions with concurrency control, based on which the isolation and temporal correctness properties can be verified by model checking, using the UPPAAL tool. By applying the proposed approach to the development of an industrial demonstrator, we validate the applicability of our approach.
|
|
| 2. |
- Castellanos Ardila, Julieth Patricia, Doctoral student, 1976-
(författare)
-
A Safety-centered Planning-time Framework for Automated Process Compliance Checking
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Safety-critical systems, whose failure could lead to catastrophic consequences, are everywhere. Not only environments with high-risk functions, e.g., nuclear power plants, are safety-critical systems. Our vehicles, medical devices that perform different kinds of treatments, airplanes, and industrial robots, are also safety-critical systems. The more harm the system can cause, the more careful the system has to be designed, implemented, and maintained. By following practices of reasonable care, typically collected within industry standards, manufacturers demonstrate that they aim at preventing safety-critical systems from failing or causing various types of damage. Thus, compliance with standards, especially safety standards, is a must-do for manufacturers of safety-critical systems.Industry standards often adopt a prescriptive approach, which focuses on process-related requirements. To comply with such standards, manufacturers have to carefully prepare process plans that properly address the applicable requirements. A compliant process plan should include the sequence of tasks mandated by applicable standards as well as the resources allocated to such tasks, e.g., personnel, work products, required tools, and methods, which are also framed with key properties. The planning task could be supported by checking that planned processes fulfill the properties set down by standards at given points.Compliance checking of process plans is rarely done for just one standard. In automotive, for instance, it is recommended that manufacturers follow at least standards for functional safety, cybersecurity, and software process improvements. Manufacturers also need to perform tailoring, i.e., select and modify requirements depending on the individual project. In safety standards, tailoring is often performed by taking into account existing safety criticality levels. Moreover, new versions of the standards, which are frequently released, demand recertification. In addition, compliance checking is not only done to one process plan. Companies commonly need to plan several processes simultaneously. Consequently, it is not easy to manually check that process plans comply with the requirements of standards.Automated compliance checking could help process engineers in such organizations to detect compliance violations and enforce compliance at planning time. Thus, the main goal of this dissertation is to facilitate automated compliance checking of the process plans used to engineer safety-critical systems against the standards mandated (or recommended) in the safety-critical context. To reach our goal, we adopt modern methods and tools, adapt them by mainly focusing on software and risk analysis process plans, and contribute to the state-of-the-art as follows:1. We identify aspects that make compliance checking of process plans demanding and formulate requirements for a technical solution to these problems. 2. We introduce ACCEPT (Automated Compliance Checking of Engineering Process plans against sTandards), an iterative and comprehensible framework for supporting process engineers to check and enforce process plan compliance. 3. We propose mechanisms for facilitating the creation and reuse of the specifications required to check process plan compliance.4. We investigate the significance of our proposed solutions by applying different validation mechanisms. As a result, our solutions show to be useful to support process engineers in the compliance checking tasks required during process planning.This dissertation's contributions aim at planting the seeds for the future development of tools that support process engineers moving towards automated compliance checking practices.
|
|
| 3. |
- Castellanos Ardila, Julieth Patricia, Doctoral student, 1976-
(författare)
-
Facilitating Automated Compliance Checking of Processes against Safety Standards
- 2019
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- A system is safety-critical if its malfunctioning could have catastrophic consequences for people, property or the environment, e.g., the failure in a car's braking system could be potentially tragic. To produce such type of systems, special procedures, and strategies, that permit their safer deployment into society, should be used. Therefore, manufacturers of safety-critical systems comply with domain-specific safety standards, which embody the public consensus of acceptably safe. Safety standards also contain a repository of expert knowledge and best practices that can, to some extent, facilitate the safety-critical system’s engineering. In some domains, the applicable safety standards establish the accepted procedures that regulate the development processes. For claiming compliance with such standards, companies should adapt their practices and provide convincing justifications regarding the processes used to produce their systems, from the initial steps of the production. In particular, the planning of the development process, in accordance with the prescribed process-related requirements specified in the standard, is an essential piece of evidence for compliance assessment. However, providing such evidence can be time-consuming and prone-to-error since it requires that process engineers check the fulfillment of hundreds of requirements based on their processes specifications. With access to suitable tool-supported methodologies, process engineers would be able to perform their job efficiently and accurately.Safety standards prescribe requirements in natural language by using notions that are subtly similar to the concepts used to describe laws. In particular, requirements in the standards introduce conditions that are obligatory for claiming compliance. Requirements also define tailoring rules, which are actions that permit to comply with the standard in an alternative way. Unfortunately, current approaches for software verification are not furnished with these notions, which could make their use in compliance checking difficult. However, existing tool-supported methodologies designed in the legal compliance context, which are also proved in the business domain, could be exploited for defining an adequate automated compliance checking approach that suits the conditions required in the safety-critical context.The goal of this Licentiate thesis is to propose a novel approach that combines: 1) process modeling capabilities for representing systems and software process specifications, 2) normative representation capabilities for interpreting the requirements of the safety standards in an adequate machine-readable form, and 3) compliance checking capabilities to provide the analysis required to conclude whether the model of a process corresponds to the model with the compliant states proposed by the standard's requirements. Our approach contributes to facilitating compliance checking by providing automatic reasoning from the requirements prescribed by the standards, and the description of the process they regulate. It also contributes to cross-fertilize two communities that were previously isolated, namely safety-critical and legal compliance contexts. Besides, we propose an approach for mastering the interplay between highly-related standards. This approach includes the reuse capabilities provided by SoPLE (Safety-oriented Process Line Engineering), which is a methodological approach aiming at systematizing the reuse of process-related information in the context of safety-critical systems. With the addition of SoPLE, we aim at planting the seeds for the future provision of systematic reuse of compliance proofs. Hitherto, our proposed methodology has been evaluated with academic examples that show the potential benefits of its use.
|
|
| 4. |
- Šljivo, Irfan
(författare)
-
Facilitating Reuse of Safety Case Artefacts Using Safety Contracts
- 2015
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Safety-critical systems usually need to comply with a domain-specific safety standard, which often require a safety case in form of an explained argument supported by evidence to show that the system is acceptably safe to operate in a given context. Developing such systems to comply with a safety standard is a time-consuming and costly process. Reuse within development of such systems is used to reduce the cost and time needed to both develop the system and the accompanying safety case. Reuse of safety-relevant components that constitute the system is not sufficient without the reuse of the accompanying safety case artefacts that include the safety argument and the supporting evidence. The difficulties with reuse of the such artefacts within safety-critical systems lie mainly in the nature of safety being a system property and the lack of support for systematic reuse of such artefacts.In this thesis we focus on developing the notion of safety contracts that can be used to facilitate systematic reuse of safety-relevant components and their accompanying artefacts. More specifically, we explore the following issues: in which way such contracts should be specified, how they can be derived, and in which way they can be utilised for reuse of safety artefacts. First, we characterise the contracts as either “strong” or “weak” to facilitate capturing different behaviours reusable components can exhibit in different systems. Then, we present methods for deriving safety contracts from failure analyses. As the basis of the safety-critical systems development lies in the failure analyses and identifying which malfunctions eventually can lead to accidents, we deem that the basis for specifying the safety contracts lies in capturing information identified by such failure analyses within the contracts. Finally, we provide methods for generative reuse of the safety case artefacts by utilising the safety contracts. Moreover, we define a safety contracts development process as guidance for systematic reuse based on the safety contracts. We use a real-world case to demonstrate the proposed process.
|
|
| 5. |
- Sljivo, Irfan
(författare)
-
Assurance Aware Contract-based Design for Safety-critical Systems
- 2018
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Safety-critical systems are those systems whose malfunctioning can result in harm or loss of human life, or damage to property or the environment. Such systems usually need to comply with a domain-specific safety standard, which often require a safety case in form of an explained argument supported by evidence to show that the system is acceptably safe to operate in a given context. Developing safety-critical systems to comply with safety standards is a time-consuming and costly process. It can often be the case that the development of the safety case is more costly than the development of the system itself.Component-based development is a method that separates the development of the components of a system from the development of the system itself. The latter is done by composing reusable components that are developed independently of the system. Safety-critical systems require that the safety case of such components is integrated in the overall safety case of the system. For this purpose, the reusable components, together with their safety case, can be described via specifications called contracts. By checking the contracts of each component of the system against each other, it is possible to determine if the components can be composed together and still fulfil the contract specifications. Contract-based design combined with component-based development has the potential to reduce the cost and time needed to develop both the system and the accompanying safety case. Such contract-based design can then be used to facilitate reuse of parts of the system as well as verifying that the system fulfils certain requirements. While contract-based design can be used to verify that a system meets certain requirements based on its contract-specification, actually assuring that the system behaves according to the verification results require additional evidence. Hence, reuse of safety-relevant components via contract-based design is not sufficient without the reuse of the accompanying safety case artefacts, which include both the safety argument and the supporting evidence.In this thesis we focus on developing the notion of safety contracts that can be used to make a contract-based design aware of the needs of safety assurance. The goals of such assurance aware contract-based design are to promote reuse of the assurance-related artefacts such as arguments and evidence, as well as to automate creation of parts of the safety assurance case. To address this, we explore the following research goals in more detail: (1) to facilitate automated contract-driven assurance, (2) to facilitate reuse of safety-relevant components and their accompanying assurance-relevant artefacts, and (3) to align such assurance-aware contract-based design with existing failure logic analysis. To meet the first goal, we identify the additional information needed for contract-based assurance and structure it in form of argumentation patterns of reusable reasoning. Then, we define a meta-model to connect the system modelling elements related to the contracts with the safety case elements, such as evidence and arguments. Based on this meta-model, we define an algorithm for automated instantiation of the proposed argumentation patterns from system models compliant with the proposed meta-model. To facilitate reuse of the assurance-related artefacts (goal (2)), we define variability on the contract level to distinguish between contracts that are relevant for all systems and those that are system-specific. Furthermore, we align the assurance-aware contract-based design with the ISO 26262 automotive safety standard and its reuse concepts. Finally, in addressing the third goal, we connect the assurance-aware contract-based design with an existing failure logic analysis and show how such combination can be used to automate instantiation of existing argumentation patterns. In a number of real-world examples we demonstrate and evaluate the feasibility of our contributions.
|
|
