In the automotive industry, automated hardware-software integration testing is of vital importance for ensuring software quality and reducing project costs. However, in practice, the generation of automated test cases for such testing faces many challenges, primarily due to the complexity, implicit, and difficulty in identifying requirement dependencies. To address this issue, this paper proposes a requirement dependency-driven automated test case generation method. This method utilizes large language models to directly extract structured models, e.g., flowcharts, from natural language requirements documents. By analyzing these flowcharts, it can accurately identify implicit requirements dependencies and generate test scenarios, thereby specifying the execution order and temporal constraints for test case generation. In a real-world case study with the Beijing Automotive Industry Corporation (BAIC), the method successfully processed 300 functional requirements and identified a total of 4731 implicit dependencies. The content accuracy rate of the generated flowcharts reached 81.24%, and the business scenario coverage rate of the test cases reached 82.67%. These results preliminarily demonstrate the effectiveness and feasibility of our approach, significantly enhancing the level of automation in automotive integrated testing and providing strong technical support and reference for related practices in the industry.

The Internet of Things (IoT) has witnessed remarkable advancements, enabling smart homes with user-centric features. To effectively articulate their personalized needs, it becomes crucial to equip end users with programming capabilities. Currently, the executable Trigger-Action Programming (TAP) rules have become the mainstream paradigm for IoT end-user programming. To simplify the creation of TAP rules, many studies have proposed various levels of requirements abstraction, yet the connections between them remain unclear. In this article, we employ a mixed-methods study to identify the preferred way of expressing end users’ requirements in practical scenarios. Subsequently, from the perspective of requirements engineering, we categorize the needs of smart home into three hierarchical levels of abstraction. Accordingly, we propose an innovative multi-level requirements description language called SH-RDL . We also address potential challenges and conduct an evaluation to validate SH-RDL ’s usability, understandability and error-prevention. This will aid in the broader adoption of IoT end-user programming.

With the rapid development of IoT technology, IoT-enabled systems, represented by smart homes, are becoming ubiquitous. In order to support personalized user requirements, such systems appeal to the end-user programming paradigm. This paradigm allows end-users to describe their requirements using TAP (Trigger-Action Programming) rules, which can be deployed on demand. However, writing TAP rules is error-prone and end-users are often unaware of the actual effects of the rules they write, given the context-sensitive nature of these effects. It is highly desirable that TAP rules can be validated before deployment. Unfortunately, requirements validation for IoT end-user programming has not received much attention so far. Therefore, this paper proposes to generate experience prototypes for IoT end-user programming using TAP rules. The difficulty lies in how to orchestrate user experience delivery service scenarios according to TAP rule and context changes, and effectively demonstrate these scenarios. We present a dynamic assembly approach for simulation model systems used for service scenario orchestration. By simulation, we synthesize desired system behaviors, system device behaviors, and context changes. Leveraging the simulation traces of each component, we employ animation techniques specifically designed to highlight user-aware changes. These experience prototypes allow end-users to directly understand the effects of the IoT-enabled systems, thereby determining whether their intentions are satisfied. Experimental results show that our approach is usable and effective for end-users and the generated experience prototypes are context-aware, capable of representing real-world service scenarios, effective, and efficient in requirements validation.

FinTech software, crucial for both safety and timely market deployment, presents a compelling case for automated acceptance testing against regulatory business rules. However, the inherent challenges of comprehending unstructured natural language descriptions of these rules and crafting comprehensive test cases demand human intelligence. The emergence of Large Language Models (LLMs) holds promise for automated test case generation, leveraging their natural language processing capabilities. Yet, their dependence on human intervention for effective prompting hampers efficiency. In response, we introduce a groundbreaking, fully automated approach for generating high-coverage test cases from natural language business rules. Our methodology seamlessly integrates the versatility of LLMs with the predictability of algorithmic methods. We fine-tune pre-trained LLMs for improved information extraction accuracy and algorithmically generate comprehensive testable scenarios for the extracted business rules. Our prototype, LLM4Fin, is designed for testing real-world stock-trading software. Experimental results demonstrate LLM4Fin’s superiority over both state-of-the-art LLM, such as ChatGPT, and skilled testing engineers. We achieve remarkable performance, with up to 98.18% and an average of 20%−110% improvement on business scenario coverage, and up to 93.72% on code coverage, while reducing the time cost from 20 minutes to a mere 7 seconds. These results provide robust evidence of the framework’s practical applicability and efficiency, marking a significant advancement in FinTech software testing.

Multi-agent systems (MASs) have garnered significant interest across various academic fields. Although MASs are widely applicable, they continue to encounter several challenges, particularly in terms of security.. Model checking, a verification technique that examines all possible system states, is employed to address these challenges. However, the state space of many practical systems can be prohibitively large, leading to exponential growth in verification time. This study introduces a new method for verifying MASs using Strategy Computation Tree Logic (SCTL) via the connective probe machine, a model of fully parallel computing. This approach is pioneering in utilizing the probe machine to speed up MAS verification, specifically allowing for the parallel resolution of SCTL formulas. Unlike conventional model checkers, our method can uncover multiple counterexamples for specified properties, facilitating the identification of various system flaws. We have developed a model checker named MC2PM based on our approach and have validated its feasibility and efficiency through experiments.

Trigger-Action Programming (TAP) is a new programming paradigm enabling end-users to customize their smart devices by defining simple trigger-action rules. While it offers appealing convenience to end-users, TAP renders devices vulnerable to operation chaos and security risk resulting from potential defects in the rules. Verifying TAP rules defined by end-users is thereby necessary to detect such vulnerabilities at the early stage. However, such rules are difficult to analyze because their executions are often device-specific and environment-driven. Existing approaches require modeling them with their host devices and running environments, which is labor-consuming and hard to be automated. Moreover, the composition of devices causes state explosion, rendering the conflict analysis time-consuming. In this paper, we first build a large corpus of TAP rules developed by end-users. Analyzing this corpus results in six types of conflicts and reveals that nearly 90% of end-users made conflicts in their customized rules, and on average, 3.7 rules contain a conflict, which concurs with the necessity of developing practical conflict analysis techniques. Empirical analysis motivates us to propose a lightweight SMT-based approach for conflict analysis from a programmatic perspective. Compared to the existing approaches, our approach does not require modeling devices; thus, it could be fully automatic and flexible in efficiently detecting various types of conflicts. We implement the approach in a tool TapChecker. We analyze 12,514 TAP rules collected from real-world TAP platforms (10,535) and laboratory experiments (1,979). Experimental results show that our approach outperforms the state-of-the-art tool regarding the number of detected conflicts and efficiency.

Dealing with the ever-growing complexity of railway systems requires scalable approaches for detecting inconsistent safety requirements in practice. Despite significant efforts to automate the requirements consistency detection, current inconsistency analysis techniques of railway safety requirements still suffer from scalability issues. This paper proposes a two-layer approach for detecting inconsistencies in time-related safety requirements of railway systems, integrating two distinct formal methods from a pragmatic perspective. At the SafeNL layer, we employ an SMT-based approach to extract conflict patterns and use them to filter out inconsistent requirements descriptions, thus avoiding the more expensive general use of the SMT-based approach. At the CCSL layer, temporal dependencies in requirements are transformed into causal relations, which are then detected for circular inconsistencies using a graph search technique. Our evaluations demonstrate the utility and scalability of our approach.

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.

Due to deeply intertwined physical and hardware/software components together with an increasing number of interconnected heterogeneous devices powered by artificial intelligence (AI) techniques, the design complexity of cyber–physical systems (CPSs) becomes skyrocketing. Model-driven engineering (MDE) methods have been proven to be effective in increasing the productivity of CPS design. However, there is still a lack of MDE approaches that enable design space exploration as well as the code generation for the design of Artificial Intelligence of Things (AIoT)-based CPSs. To mitigate the situation, this article presents a unified modeling language named AIoTML for AIoT-based CPSs, which enables the construction of AI-based components across different modeling levels for the purposes of intelligent sensing and control. By extending the constructs of state-of-the-art domain-specific language (DSL) ThingML, AIoTML can seamlessly unify the modeling of both autonomous executions of AIoT devices and their surrounding physical environment, which facilitates both platform-independent simulation and control optimization for platform-specific CPSs. The compiler developed for AIoTML provides a family of code generators to support the construction of digital twins on various heterogeneous target AIoT platforms. Comprehensive evaluations on two complex real-world designs demonstrate the effectiveness of our AIoTML approach in the fast development of AIoT-based CPSs with high control quality.

As a promising requirement-level specification language for timing behavior modeling, the clock constraint specification language (CCSL) has become popular in the model-driven design community for safety-critical embedded systems. However, due to the skyrocketing design complexity, in practice, it is hard for requirement engineers to accurately construct requirement models with expected timing behaviors using CCSL, especially, for safe timing behaviors. Although more and more CCSL synthesis approaches are designed to facilitate the generation of CCSL specifications, most of them cannot be used directly for the synthesis of requirements models. This is because existing CCSL synthesis methods: 1) focus on filling the holes of CCSL constraints rather than completing requirements models and 2) rely heavily on limited observations of system behaviors, while the (temporal) safety properties of target systems are neglected. To address these issues, this article proposes a novel method that enables the automated synthesis of safe timing behaviors for requirements models. By specifying the safety timing properties of target systems using safely-LTL, our approach adopts CCSL as an intermediate representation of requirement synthesis, where incomplete requirements models coupled with safely-LTL-based properties are encoded into CCSL constraints with holes. Guided by the samples (expected behaviors) provided by requirement engineers, our approach can automatically figure out the complete version of incomplete requirements models. Comprehensive experimental results on two complex case studies demonstrate that our approach can not only quickly and efficiently synthesize requirement models but also guarantee that the synthesized models satisfy specified safety properties in Safely-LTL form.

Consistency verification of safety requirements is crucial for the success of safety-critical systems, particularly railway systems. However, this task often requires significant time spent on interaction and communication between domain experts, who possess in-depth knowledge of safety requirements in a specific domain, and formal experts, who have the necessary skills to apply verification tools and techniques. To enhance time efficiency and productivity, we propose an approach to empower domain experts with formal methods for verifying safety requirements’ consistency. This involves transforming natural requirements into formal models and using formal methods for verification. The approach also localizes inconsistent requirements to provide feedback to domain experts. Communication between domain experts and formal experts can be facilitated through the pattern language SafeNL. By adopting this approach, domain experts can utilize formal verification without extensive consultation with formal experts. Two practical case studies with CASCO Signal Ltd. validate its effectiveness, practicality, as well as a significant reduction of time compared to traditional methods (at least 90% reduction). This reduction in time is primarily due to reduced communication needs and more efficient localization. Evaluations show that SafeNL is user-friendly and the approach performs well in modular systems while scalability is somewhat limited.

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.

The rapid development of Internet of Things (IoT) technology makes smart homes a reality, where many user-centered service scenarios are yet to be built. For such applications, it is of utmost importance to let end users express their needs easily on the one hand, and these users’ expectations can be interpreted by the smart home systems accurately on the other hand. Unfortunately, existing requirements languages are not for end users to express their needs in daily terms. An easy but expressive requirements language is required. This paper carries out a survey on suitable and expressive requirements description language for smart homes. Based on the results, a user requirements description language Smart3E is designed for enabling end user expressions. This paper also puts forward the challenges that are needed to be addressed when allowing end users to express their needs freely in smart home domain.

Software requirements are the criteria for the correctness of the software behaviors. How to verify the correctness of the requirements is a big challenge in requirements engineering. Among various requirements approaches, the environment modeling based requirements engineering(EBRE) gains great popularity due to its explicit environment model. However, it still lacks of a formal approach to verify the correctness of the requirements models proposed in EBRE. Event-B is a popular formal method employing step-wise refinement to construct system models and verify their correctness according to the system requirements. This paper combines EBRE with Event-B to merge the advantages of the two methods. On the one hand, we transform the EBRE models to the initial Event-B model to guide the further design and development of the system. On the other hand, the transformed Event-B model can provide formal proof on the consistency of the requirements model. We also implement a plug-in tool on the Rodin platform to realize the automatic transformation from EBRE models to Event-B model and to commit a formal verification on the correctness of the transformed requirements model.

For Cyber-Physical systems (CPSs), timing requirements are as important as functional ones. They should be specified with a vocabulary as close as possible to the domain experts, and not necessarily limited to physical time. Multiform time is an abstract form of time that encompasses both physical and logical time. We argue that it gives the right abstraction level to remain close to the requirement provider needs. We choose the Problem Frames (PF) notation to describe the functional requirements for CPS, and we propose a multiform time based approach to elicit timing requirements. This paper gives (1) an extension of PF with multiform time; (2) a semi-automatic elicitation process; and (3) an automatic way to check the consistency of the resulting timing specification using NuSMV. This proposal is illustrated on a spark-ignition system in which time properties are expressed relative to the rotation degree of the engine camshaft instead of a more classical time unit (seconds).

Deep Neural Networks (DNN) has gained great success in solving several challenging problems in recent years. It is well known that training a DNN model from scratch requires a lot of data and computational resources. However, using a pre-trained model directly or using it to initialize weights cost less time and often gets better results. Therefore, well pre-trained DNN models are valuable intellectual property that we should protect. In this work, we propose DeepTrace, a framework for model owners to secretly fingerprinting the target DNN model using a special trigger set and verifying from outputs. An embedded fingerprint can be extracted to uniquely identify the information of model owner and authorized users. Our framework benefits from both white-box and black-box verification, which makes it useful whether we know the model details or not. We evaluate the performance of DeepTrace on two different datasets, with different DNN architectures. Our experiment shows that, with the advantages of combining white-box and black-box verification, our framework has very little effect on model accuracy, and is robust against different model modifications. It also consumes very little computing resources when extracting fingerprint.

Analysis of spatial behaviors of safety-critical systems attracts more and more attention in the filed of cyber physical systems and image processing. The major problem is expressiveness and verifiability for modeling and analysis of spatial behaviors. In order to verify the satisfiability problem of spatial properties, in this paper, we propose a novel topometric model through inducing a topological space with metric distance. For the spatial logic, we specify spatial properties with S4u in continuous regions, which are encoded S4u formula to RCC-8 relations, and discrete spatial regions, whose evolution is achieved through extending S4u with spatial near and until, named S4ue. We present a spatial model checking algorithm to verify if an S4u spatial term or formula satisfies the topometric model. We exemplify the applicability of the approach on obstacle avoidance-based path planning of robots.

We study the use of Multiform Logical Time, as embodied in Esterel/SyncCharts and Clock Constraint Specification Language (CCSL), for the specification of assume-guarantee constraints providing safe driving rules related to time and space, in the context of Automated Driving Assistance Systems (ADAS). The main novelty lies in the use of logical clocks to represent the epochs of specific area encounters (when particular area trajectories just start overlapping for instance), thereby combining time and space constraints by CCSL to build safe driving rules specification. We propose the safe specification pattern at high-level that provide the required expressiveness for safe driving rules specification. In the pattern, multiform logical time provides the power of parameterization to express safe driving rules, before instantiation in further simulation contexts. We present an efficient way to irregularly update the constraints in the specification due to the context changes, where elements (other cars, road sections, traffic signs) may dynamically enter and exit the scene. In this way, we add constraints for the new elements and remove the constraints related to the disappearing elements rather than rebuild everything. The multi-lane highway scenario is used to illustrate how to irregularly and efficiently update the constraints in the specification while receiving a fresh scene.

Due to the mobility of autonomous vehicles and changing context through time, the constraints in safe driving rules specification need to be irregularly updated for monitoring the trajectory plan. This is not assumed in the Spatial-Temporal Logic. This paper proposes a novel approach to build the specification of assume-guarantee constraints providing safe driving rules related to time and space, in the context of Automated Driving Assistance Systems (ADAS). The novelty lies in that the specification adopts Multiform Logical Time to express the time constraints and provides spatial events generated by interactions on area trajectory for expressing space constraints. We propose the safe specification patterns at a high-level that provide the required expressiveness for safe driving rules. In these patterns, logical time provides the power of parameterization to express rules, before instantiation in low-level simulation contexts. The specification finally could be used to generate monitors that are executed on lower-level simulation engines with physical and topological features.

Combining spatial and temporal primitives together is quite useful to specify dynamic behaviors of cyber-physical systems. The ability to represent spatio-temporal properties by means of formulas in spatio-temporal logics has recently found important applications in various fields, such as runtime verification, parameter synthesis, contract-Based design. In this paper, we present a spatio-temporal specification language, STSL, by combining Signal Temporal Logic (STL) with a spatial logic S4u, to characterize spatio-temporal dynamic behaviors of cyberphysical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatiotemporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL combines the power of temporal modalities and spatial operators, and enjoys important properties such as safety and liveness. We provide the falsification problem through extending Lemire's algorithm and a parameter synthesis procedure by calling the simulated annealing algorithm. We demonstrate the proposed approaches on adaptive cruise control system and path planning of quadrotors.

UML interactions, aka sequence diagrams, are frequently used by engineers to describe expected scenarios of good or bad behaviors of systems under design, as they provide allegedly a simple enough syntax to express a quite large variety of behaviors. This paper uses them to express formal safety requirements for safety critical systems in an incremental way, where the scenarios are progressively refined after checking the consistency of the requirements. As before, the semantics of these scenarios are expressed by transforming them into an intermediate semantic model amenable to formal verification. We rely on the Clock Constraint Specification Language (CCSL) as the intermediate semantic language. An SMT-based analysis tool called MyCCSL is used to check consistency of the sequence diagrams. We compare these requirements against actual execution traces to prove the validity of our transformation. In some sense, sequence diagrams and CCSL constraints both express a family of acceptable infinite traces that must include the behaviors given by the finite set of finite execution traces against which we validate. Finally, the whole process is illustrated on partial requirements for a railway transit system.

Describing spatio-temporal behaviors of cyber-physical systems attracts more and more attention in the filed of intelligent transportation systems and biological systems. The major problem is expressiveness and verifiability for modeling and analysis of spatio-temporal behaviors. In order to verify spatial and spatio-temporal behaviors, in this paper, we propose a methodology to model the evolution of spatial scene snapshots and verify the spatio-temporal models. Firstly, we define a novel Topograph through inducing Bigraph in topological space to characterize cyber-physical systems and verify the model against patterns specified with S4uformulas. Secondly, for spatio-temporal verification, we extend Topograph in dense time, named Temporal Topograph, to describe the evolution of spatial objects, which are verified against spatio-temporal specification language. We evaluate the applicability of the approach on CBTC-based intelligent transportation systems.

The Clock Constraint Specification Language ( CCSL ) is a formalism for specifying logical-time constraints on events for the design of real-time embedded systems. A central verification problem of CCSL is to check whether events are schedulable under logical constraints. Although many efforts have been made addressing this problem, the problem is still open. In this paper, we show that the bounded scheduling problem is NP -complete and then propose an efficient SMT-based decision procedure which is sound and complete. Based on this decision procedure, we present a sound algorithm for the general scheduling problem. We implement our algorithm in a prototype tool and illustrate its utility in schedulability analysis in designing real-world systems and automatic proving of algebraic properties of CCSL constraints. Experimental results demonstrate its effectiveness and efficiency.

Consistency verification of safety requirements is an important but still challenging task for safety-critical systems such as rail transit systems. That is mainly because requirements are typically written in natural language and with strong time constraints. Driven by the practical need from industry, in this paper we propose a systematic approach to specify safety requirements in a quasi-natural language and automatically verify their consistency using formal methods. Specifically, we define a domain specific language SafeNL to specify safety requirements, and then automatically transform them into formal constraints defined in the Clock Constraint Specification Language (CCSL). The transformed constraints can be automatically and efficiently verified by model checking. We conduct two practical case studies to analyze the safety requirements of an interlocking system in CASCO Signal Ltd. Results of the studies show the validity and utility of our approach can pragmatically contribute to industrial practice. We also report some lessons learned from case studies.

In requirements engineering (RE), there are three essential descriptions, i.e., requirements, specification and domain properties. Their relationship is proposed by Jackson et al, and verified in various requirements approaches. However, at present, there is no formal verification for the relationship in the Problem Frames (PF) which is a well known approach in the RE. Our previous work based on the PF explicitly captures the three descriptions. Based on that work, this paper further formalizes the three descriptions using Communicating Sequential Process (CSP), transforms the relationship into two "refines", and verifies them with Process Analysis Tool (PAT). The verification ensures that the machine which behaves as in the specification installed in a specific domain will satisfy the requirements.

Formal methods have been applied widely to verifying the safety requirements of communication-based train control (CBTC) systems, while the problem situations could be much simplified. In industrial practices of CBTC systems, however, huge complexity arises, which renders those methods nearly impossible to apply. In this paper, we aim to reduce the state space of formal verification problems in zone controller, a sub-system of a typical CBTC. We achieve the simplification goal by reducing the total number of device variables. To do this, two projection methods are proposed based on problem frames and constraints, respectively. The problem frame-based method decomposes the system according to sub-properties through functional decomposition, while the constraint-based projection method removes redundant variables. Our industrial case study demonstrates the feasibility through an evaluation, confirming that these two methods are effective in reducing the state spaces of complex verification problems in this application domain.

For modelling hybrid systems, we have extended Event B based on its framework with the differential event. The differential event describes continuous behaviors of hybrid systems by differential equations and evolution constraint, whose proof obligations provide dynamical properties of a model. In order to ensure the safety and reliability of a model, proof obligations should be proved. It is difficult to prove proof obligation in state space, because there is no a complete method to solve differential equations in the field of mathematics. Thus we proposed an approach to proving proof obligation based on differential invariants. It is to avoid uncontrollable computation on solving differential equation. The main result is that we prove some theorems for proving proof obligations involving differential events within the framework of refinement calculus. Lastly, through the case of the Train Control System, we further show that the approach is well suited.

The integration of formal methods and requirements analysis increases the dependability of safety-critical systems. However it is still very difficult to obtain all of the safety requirements in practice, and formally construct the safety requirements model as well. In this paper, we propose an approach to capture safety requirements and formally describe them by classifying and developing safety requirements specification patterns. Our classification is a result of extracting safety properties from a variety of sources, such as interlocking tables and existing safety relevant functional requirements of railway interlocking system. They contain safety properties at analysis level and design level respectively. Furthermore, safety specification patterns based on the classification are used to formally describe and organize the safety requirements for formal verification. Finally, a tool called SRSV has been developed to enhance the process from deriving safety requirements to verifying. We applied it to the interlocking system at Mohe station in China, and the generated safety properties were then checked to hold by the verification tool.

For many old buildings in the world, due to the legacy devices problem, it is hard to supply appropriate energy for them.In order to reduce the energy consumption of buildings under the premise of satisfying user requirements, we use software control systems whose core part is the scheduling strategy, to reconstruct them.It is time consuming to choose a good scheduling strategy due to many uncertain factors, among which user actions are of the most influence.In this paper, we propose an Support Vector Machine (SVM) based approach to explore the relation between user action and the best scheduling strategy of a control system.The main contributions include:(1) obtaining the sample set by collecting data at the model level using Statistical Model Checking (SMC) based method; (2) using SVM algorithm to learn the relation model between user actions and the best scheduling strategies; and (3) applying the relation model to predict a best scheduling strategy.Finally a real case study is conducted showing the efficiency of our approach.

The safety properties of Cyber-Physical Systems have characteristics of both time and spatial attributes. Although various hybrid logic languages have been proposed to represent and reason both time and spatial attribute, most of them are not concerned on the quantitative problem which is important for mission-critical CPSs to specify and verify safety properties. In this paper, we propose a language named metric temporal-spatial logic (MTSL) to solve the problem. MTSL is the combination result of the metric temporal logic (MTL) and the spatial logic S4u. It can represent and reason CPS safety properties with both temporal and spatial attributes in a time quantitative manner. Based on different expressivity requirements, we define two kinds of MTSL languages named MTSLtPC and MTSLtOC. Their computational complexity of satisfiability problem are analysed. Moreover, in order to construct a decidable metric temporalspatial logic which can be used to define safety properties, we also point out that one may use safety metric temporal logic (SMTL) as the temporal language. The application of MTSLs are illustrated by case studies coming from transportation domain.

Energy consumption evaluation is one of the most important steps in Cyber-Physical Energy System (CPES) development. However, due to the lack of accurate and effective modeling and evaluation approaches considering the uncertainty of environment, it is hard to conduct the quantitative analysis for the energy consumption of CPESs. To address the above issue, this paper proposes an environment-aware energy consumption evaluation framework based on the Statistical Model Checking (SMC). In our framework, the environment uncertainty of CPESs is modeled using the Stochastic Hybrid Automata (SHA). In order to describe various environment modeling patterns, we create a collection of parameterized SHA models and save them to a domain specific environment ontology. Based on the domain environment ontology and user designs in the form of UML sequence diagrams and activity diagrams, our framework can automatically guide the construction of CPES models using networks of SHA and conduct the corresponding energy consumption evaluation. A case study based on an energy-aware building design demonstrates that our approach can not only support the accurate environment modeling with various uncertain factors, but also can be used to reason the relations between the energy consumption and environment uncertainties of CPES designs.

Modeling and Analysis of Real-Time and Embedded systems (MARTE) is a profile of United Modeling Language (UML), which provides support for specification, design and verification for Real-Time Embedded Systems (RTES). MARTE sequence diagram can deal with both discrete and dense time in which a clock can be either chronometric or logical. However it lacks the ability to describe the continuous behavior of a hybrid system. We propose a new method named Hybrid MARTE Sequence Diagram (HSD) to describe the communication between participants and the continuous evolution within the execution occurrence of a hybrid system. HSD combines the time model from MARTE and specification of the time-continuous behavior aspects from hybrid automata with MARTE sequence diagram. It improves the MARTE sequence diagram in that: the logical time and the chronometric time are unified. Besides, the description of continuous evolution of a hybrid system is provided. We firstly extend the basic MARTE elements to support both discrete and continuous aspects. Then we define the formal syntax and semantics of HSD based on hybrid transition system. Using this new method, we model an industrial application named Train Position Determination (TPD).

Automation and high coverage are two essential industrial technical requirements of qualified testing method for safety-critical systems. The ioco-testing method is a sound and well-defined formal automation testing technique for labelled transition system. However, when we apply this method to a train control system developed by our industrial partner, we find that some testing requirements are not covered for certain testing objects. Further analysis has shown that the ioco-testing method only generates test cases based on explicit specified system behaviors which may result in low coverage when the implementation under test includes code branches used to deal with faults which can't be defined thoroughly in the specification in practices. Therefore, we propose a labelled transition system testing method based on specification mutation to improve safety-critical system testing coverage. We firstly define the mutation operators for the Input output symbolic transition system (IOSTS) modeling language, then we construct the corresponding test generation algorithm and translate the derived test cases into xml files which can be directly applied to the implementation under test in a simulation and test platform developed by our partner. Preliminary experiments on a safety-critical function named train position determination have shown about 28.5% improvement on the testing coverage.

The Problem Frames (PF) approach is a well-known approach for describing, analyzing and structuring problems in requirements engineering. It defines certain patterns of problems to be problem frames which have solutions. The real world problems are solved by decomposing to sub-problems which could be matched against problem frames. However, whether existing problem frames is enough for covering all problems is undecided. In this paper, we propose to recognize problem frames in a specific application domain by using feature models. As feature models could link to solution space, our approach bridges the gap between problem frames and solution space. The newly constructed problem frames could be used to analyse problems. We illustrate their usage by presenting a problem frames based problem analysis which include problem descriptions and matches. Because our new problem frames are high level, the real world problems do not need to be decomposed before matched.

It is well acknowledged that environment plays an important role in requirement derivation. However, at present the time-continuous properties of the environment are of little concern. Our previous work modeled the time-continuous environment by constructing a software environment ontology. This paper further presents an approach for deriving software requirements specification with time using software environment ontology. Experiments are conducted by deriving different software requirement specifications under different situations. They are simulated with Simulink. The simulation results show that the software behaviors can be more accurately determined with respect to time-continuous environment by using time as a measurement.

AADL (Architecture Analysis and Design Language) is widely used in the area of modeling and analysis. However, it is not so convenient to describe a hybrid system with AADL. In this paper, we propose an approach to construct an annex of AADL, thus to facilitate the modeling and analysis of hybrid system. The syntax and semantics of hybrid AADL are provided. Additionally, we developed a hybrid system modeling plug-in to OSATE, which is an AADL supporting tool. Our approach, as well as our tool, is successfully used in the development of a lunar rover control system for the institute of China Aerospace Science and Technology.

In component-based architecture, a component is a unit of computation or a data store. Connectors are architectural building blocks used to model interactions among components. However, in some particular complex real-time systems, it is non-determinate and confused to distinguish some modules functioning as components as well as connectors. Therefore, a unified model method is demanded to describe those modules. In this paper, we propose a method to divide components into reactive and active component based on providing or requiring services when they interact with each other. A reactive component provides services and could call services of other reactive components. Active components call reactive components and are used to coordinate reactive components. Active and reactive timed automata are unified defined by extending timed automata to denote them. Then, we redefine the component composition language and present the semantics of composition of timed automata. A case study of Train Integrity Detection System illustrates the usage of our unified models for active and reactive components.

Precisely describing complicate interaction process is still an open problem in MARTE(Modeling and Analysis of Realtime Embedded System). In this paper, we propose an approach to modeling interaction behaviors to enhance MARTE modeling ability. MARTE is published by OMG(Object Management Group) in Aug, 2010 as a standard modeling language for modeling real time and embedded system. Our approach is based on timed CSP(Communicating Sequential Processes). To describe the multiform time structure in MARTE, we make an extension to timed CSP. The syntax and semantics of the communicating process specification are given and also the laws, the trace model and the failures model are defined. One of the main advantages of our method is to help people to modeling the complicate interaction process with process algebra, thus to simplify the modeling and verification of the interaction and concurrent behaviors in real-time and embedded systems between different processes. The approach is applied to model and analyze a Train Over Speed Protection System for Shanghai Bell Company.

As the embedded systems are becoming more and more complex, requirements engineering approaches are needed for modeling requirements, especially the timing requirements. Among various requirements engineering approaches, the Problem Frames(PF) approach is particularly useful in requirements modeling for the embedded systems due to the characteristic that the PF pays special attention to the environment entities that will interact with the to-be software. However, no concern is given on timing requirements of the PF at present. This paper studies how to add timing constraints on problem domains in the PF. Our approach is to integrate the problem representation frame in the PF with the timing representation mechanism of MARTE(Modeling and Analysis of Real Time and Embedded systems). A unified problem frame modeling process integrated with timing constraints is provided, and problem frame requirements with timing constraints expressed by MARTE/CCSL(Clock Constraint Specification Language) and clock construction operators are obtained.