Some examples of systems and their organizations that have ignored or violated human values have caused very devastating and widespread damage. To prevent these incidents, operationalizing human values in systems transforms the values into concrete concepts such that they can be validated. There are several challenges such as a lack of techniques to integrate values, mechanisms to trace values, formalized perspective of values. To address these challenges, we propose Ont4Sys, an ontology-based tool of semantic representation and verification for traceability models with human value. Our research uses the formal theory Ontology to integrate value into the model and traces value under traceability’s guidance. The verification and labeling algorithm is provided to verify values and help with inspections. Two subject systems are selected for feasibility and accuracy evaluation. The experimental results show that our approach can effectively verify human values; moreover, based on traceability, there is at least a 50% reduction rate in model size to help with inspections. The labeling algorithm ensures high recall while minimizing the "noise" that is detrimental to the user’s understanding of the system.

Safety analysis is a crucial process in developing safety-critical systems, allowing the identification of potential design issues that may lead to hazards. Automation of this process has become the focus of research in the critical system domain due to the growing complexity of systems. This paper proposes a Component Fault Trees (CFTs) based Failure Mode and Effects Analysis approach for Architecture Analysis and Design Language (AADL) models. First, we propose a methodology for directly generating CFTs from AADL models to display the overall failure behavior of the system. Then we extend the Error Model Annex Version 2 (EMV2) with DFMEA property to express the assessment criteria of error formally, and conduct Design Failure Mode and Effects Analysis (DFMEA) whose core step is guided by CFTs. We discuss our approach with its tool support and evaluate its applicability in driving the design of safety-critical systems through a case study.

The decision-making process in autonomous driving systems encounters large uncertainties with environmental changes and needs to face the complex spatio-temporal evolution of multiple objectives.Formal analysis and verification are crucial to establishing reliable and safe standards.In this paper, we propose an extension of the clock constraint language CCSL to construct spatio-temporal constraint and autonomous driving safety specifications, leveraging various autonomous driving scenarios.Additionally, we introduce probabilistic spatio-temporal events and devise extensions for driving specifications that incorporate stochasticity.This specification is converted to the UPPAAL-SMC model for facilitating formal modeling and verification.Specific schemes and verification are given in conjunction with a typical autonomous driving scenario.

Testing is an essential part of the software development of Safety-Critical Systems (SCSs). Since it can automatically generate test cases using the system requirement models, Model-Based Testing (MBT) is suitable for SCSs. However, most of the existing system modeling languages for SCSs mainly focus on representing functional requirements rather than safety, e.g., SysML. In this paper, we first propose a modeling language, Safety SysML State Machine (S2MSM), to guarantee safety during the requirement modeling stage. Second, we propose a model transformation algorithm to transform the S2MSM model into an intermediate model. Then, we design a time flow operation sequence that simulates the external real-time environment. Finally, we generate test cases from the intermediate model according to the MC/DC criterion and time flow operation sequence. We conduct a case study on a real-world SCS application to demonstrate the effectiveness and efficiency of the proposed approach.

One of the major challenges confronting System Modeling Language(SysML) is that it cannot always provide verifiable guarantees of formalization and rigorousness.To verify model designs, the research of transformation from SysML to ontology emerges because of ontology's formal standards and verifiability obtained by ontology reasoners.However, existing transformation approaches are mostly limited to a single view without traceability or lack a clear process so that it can't be automated.In this paper, we propose a novel approach to maintain precious traceability between requirements and model multi-views design based on ontology.In addition, our approach contains a normative process of ontology building in support of an automated implementation.We use this approach to obtain the ontology of a safety-critical system and carry out the ontology evaluation experiment, whose results demonstrate the feasibility and efficiency of our approach.