# Multiclock Constraint System Modelling and Verification for Ensuring Cooperative Autonomous Driving Safety

Authors: Jinyong Wang; Zhiqiu Huang; Xiaowei Huang; Yi Zhu; Fei Wang
Journal: Journal of Advanced Transportation
 (2020)

---

## Abstract

CADS (cooperative autonomous driving systems) are software-intensive and safety-critical reactive systems and give great promise to our daily life, but system errors may not be identified in the design stage until the implement stage, and the cost to correct them will be more expensive later than the early stage. For designing trustworthy autonomous software systems, we have to deal with multiclock constraint models. SysML (System Modeling Language) meets increasing adoption in order to carry out system-level modelling and verification against abstract representations, but it suffers from semantic ambiguities in the design of safety-critical autonomous systems. The main objective is to investigate methods for coping with the design and analysis models simultaneously and to achieve semantic consistency based on mathematical foundations and formal model transformation. In this paper, we propose a method to combine the requirement modelling process with analysis process together for CADS safety and reliability guarantee. Firstly, we extend SysML metamodels and construct SysML profile for the CADS domain that could improve modelling correctness and enhance reusability. An instantiated CADS model has been designed by means of adopting a profile containing different key functional and nonfunctional attributes and behaviors. Secondly, we define formal syntax and semantic notations for modelling elements in the SysML state machine diagram and show transformation rules between the state machine diagram and the CCSL (Clock Constraint Specification Language) model. Semantic preservation is also proved using the bisimulation relation between them for rigorous mapping correctness. Thirdly, a cooperative autonomous overtaking driving case study on the highway scenario is used for illustration, and we use the tool TimeSquare to simulate CCSL specification execution traces at the system design stage.


---

## Body

## 1. Introduction

It can be anticipated that unmanned intelligent systems are increasing rapidly. They can adapt to hostile or hazardous environment and accomplish some extreme tasks, which are difficult or impossible for humans, such as dangerous conditions, extreme speed action or long-duration flights, and cloudy or inclement weather [1]. In recent years, CADS (cooperative autonomous driving systems) are widely used in the connected traffic situation. This application can improve traffic safety and congestion by exchanging interior- and intervehicle communication data. CADS require frequent interaction with surrounding vehicles and the environment. They are the implementation of reactive and control systems and belong to globally asynchronous and locally synchronous systems. We should endeavor in proposing a modelling method for multiclocked and distributed autonomous systems. So, we can analyze behavior events through doing multiclock system verification to identify design errors and predict unexpected faults.Model-driven and model verification are main techniques for developing safety-critical cooperative and autonomous cyber-physical systems. Autonomous systems can decide what to do or when to complete desired missions individually or collaboratively and often continuously interact with the environment. Safety-related properties, i.e., bad or unexpected events, can never happen during software execution time and play an important role in people’s life and property. When we develop an autonomous system, most of errors are generated during the design stage. In addition, system design and analysis are separated from each other, so it will be very expensive and time-consuming to cope with system errors until the implementation stage. SysML (System Modeling Language) is a widely used modelling approach to support discrete event system engineering, and CCSL (Clock Constraint Specification Language) is the most commonly used language for multiclock behavioral representation. The development and verification of formal multiclock constraint models require deep knowledge about CCSL. We can take full advantage of the two modelling languages just mentioned and show that behavioral models developed in the SysML state machine diagram can be transformed into equivalent CCSL multiclock models so that it is natural and conducive to apply SysML design generality and CCSL verification capability [2].The complexity of autonomous software systems results in the bottleneck of rigorous specification and verification. Especially, in the first step of software requirements engineering, natural language expressions are low levels consistency and can lead to ambiguity. Although formal languages provide consistent and precise syntax and semantics, it remains a difficult mission for stakeholders to understand and communicate [3–5]. The most shared way to develop safe autonomous systems consists in model-driven designing approach. Model transformation is the prime technique during the process of model-driven software development. The latest practical solution in model transformation is semantic equivalence proof, which can help users to comprehend complicated software systems. We should give special emphasis about model verification to prove semantic consistency and properties preserved in the target model. There are three kinds of common model verification techniques, i.e., formal model checking, theorem proving, and model simulation. The main limitation of theorem proving is that it is short of complete automation and needs a lot of human interaction. Although formal model checking can run automatically, it suffers from significant defect, for example, state explosion problem [6]. Model simulation is based on symbolic execution which requires the operational semantics defining model behavior in reaction to input stimuli. It is a widespread technique helping to generate certification evidence through verifying assumptions.However, more and more features, such as concurrency, distribution, heterogeneity, and multicore, have been introduced into autonomous software, which lead to three important challenges in the development of CADS. Firstly, it is important and difficult to mitigate ambiguities between nonformal language requirements and formal specification. Natural or semiformal language statements often result in misinterpretations and may lead to ambiguities [7, 8]. Secondly, designing cooperative autonomous systems is a multidisciplinary problem because we should consider dependability requirements, emergent phenomena, accountability for accidents, and supporting evolution. It is essential to propose a special modelling language profile, which customizes reference metamodel for a particular cooperative autonomous domain [9, 10]. Last but not the least, the most challenging issue is to prove semantic preservation between the source and the target model [11, 12]. Complexity of CCSL semantics makes it hard to prove semantics consistency for model transformation. Rigorous proof for semantics preservation will ensure the correctness and effectiveness of communication and understanding among application domain experts, model designers, and system analysts [2, 13, 14].For these three challenges, our research focuses on multiclock autonomous system specification and simulation to overcome the problems mentioned. There are three main contributions in this article. Firstly, we provide a cooperative autonomous system modelling SysML profile including a conceptual model and interrelationships. So, we can enjoy the benefits of using SysML for breaking down the complex systems into discrete pieces, which are conducive to communicate with disparate developers on different platforms and enhance the understandability of CADS stakeholders. Secondly, we give the formal syntax and semantic notations for modelling elements in SysML and transform the conducted state machine diagram model into mathematically based formal CCSL model. The benefit of transformation is that we can use different models and software safety and reliability analysis tools without having to repeat modelling processes. After presenting syntax and semantics of the SysML state machine and CCSL, we must prove behavior preservation through the proof of bisimulation relation. Thirdly, in order to obtain certification evidence for complex and safety-critical autonomous systems, we adopt a commonly used simulation method in this work. The simulation tool TimeSquare is specifically designed to verify and validate multiclock constraint CCSL models, and we make full use of it to generate execution simulation results to analyze corresponding multiclock constrain autonomous systems.The structure of this paper is as follows:Section 1 introduces the background and objectives of this paper. In Section 2, motivations and connections with the related work of multiclock constraint autonomous system modelling and verification are given. In Section 3, we present multiclock constraint systems and describe relevant state-of-the-art concepts used for systems’ specification and verification, such as model-driven method, CCSL, simulation tool TimeSquare dedicated to CCSL analysis, and motivating scenario. We present the state machine model for CADS, semantic mapping rules from the state machine to the formal CCSL model, and bisimulation proof for behavior equivalence in Section 4. In Section 5, a case study, autonomous overtaking in the highway scenario, demonstrates effectiveness of the proposed method. In the last part of this paper, Section 6 discusses conclusions by summarizing contributions and points out future work.


## 2. Motivation and Related Work

With the rise and development of advanced driver assistance systems, from almost pure human control to fully autonomous decision with minimal human interaction, they are now being deployed in safety- and mission-critical scenarios. In safety-critical systems, the massive use of software is increasingly improving our daily life, and autonomous vehicle manufacturers and suppliers already design and ensure safety-critical software. Safety is one of the major nonfunctional properties, and tremendous expectations and increasing deployments lead us towards using formal specification and formal verification to obtain evidence for cooperative and autonomous systems [15]. In this section, we describe motivation and short review research related to modelling and verification for multiclock autonomous systems.


### 2.1. System Modelling and Model Transformation

Autonomous driving system is a kind of multiclock constraint system, so we should provide rigorous modelling methods to ensure safety and correctness. Firstly, we discuss relevant work involving system modelling and model transformation. Bochmann et al. [16] presented the controller synthesis and compositional verification for multilane traffic maneuvers. Arcile et al. [17] proposed a framework using timed automata and model checker UPPAAL (developed by Uppsala University and Aalborg University) to verify safety and robustness properties. Kamali et al. [18] constructed a spatial controller using hybrid agent architecture to model autonomous lane-change maneuvers for real-time and spatial properties. Webster et al. [19] introduced an approach combining formal verification and flight simulation for autonomous unmanned aircraft. Akhtar and Missen [20] demonstrated a method to construct a stepwise refinement multiagent model using process algebra from abstract to concrete concepts incrementally and showed how to ensure the safety and liveness properties for concurrent and interacting cooperative autonomous systems. The work in [21] introduced an abstract model for autonomous urban traffic scenarios using multilane spatial logic and showed that controllers modelled by extended timed automata can be proved safe using spatial reasoning at intersections. The aforementioned papers mainly use formal modelling methods directly at the beginning of requirement engineering. However, semiformal modelling can bridge the gap between natural requirements and formal models.Now, we will briefly discuss the relationships between our work and existing work about modelling of cooperative autonomous systems. Bernardi et al. [22] extended the UML profile, which can specialize for the railway domain and then used model transformation to generate repairable fault tree and Bayesian network models. Kapos et al. [23] explored a declarative approach and converted query/view/transformation-relation SysML model to executable simulation models, fully conforming model-driven architecture concepts. Caltais et al. [24] wanted to link two worlds of modelling and formal verification through providing transformation rules from SysML to Promela and prove the correctness based on ATL- (Atlas Transformation Language-) based transformation. Dickerson et al. [25] proposed a transformation metamodel between the UML activity model and fault tree model for end-to-end safe development process. Alshboul and Petriu [26] proposed an approach to automatically transform SysML into fault tree implemented in ETL (Epsilon Transformation Language), which can realize the purpose to integrate safety analysis within the system development process. Dias et al. [27] translated software architecture description language based on SysML and specialized profiles to process calculus CSP (communicating sequential process), and the translation can guarantee safety and liveness properties. The aforementioned works show the latest trend of model-based system development modelling and SysML model transformation for software-intensive systems. However, there is still lack of research on model transformation methods for multiclock systems, and we should provide cooperative autonomous system modelling profile and focus on transformation mapping rules for multiclock constraint time-critical systems, which is the first motivation of our work.


### 2.2. Multiclock System Specification and Semantic Equivalence

After the natural language requirement model is conducted, developers need to verify correctness and confirm whether it meets the customers’ expectations. In this section, we review existing works about multiclock specification and semantic equivalence.Multiclock timing behavior is critical for real-time cyber-physical systems. In order to analyze them early in the design stage, Goknil et al. [28] proposed a method that makes model transformation twice for formal model checking using model checker UPPAAL. The work in [29, 30] presented an approach mapping CCSL to timed input/output automata to verify safety-critical properties. The work in [31] proposed a method to combine synchronous specification language Esterel to perform validation through observers executing CCSL specification. [32–34] extended CCSL with the stochastic semantics and translated it into UPPAAL models to perform formal verification for verifying stochastic and dynamic behaviors. The work in [35] translated probabilistic CCSL into proof objective models for supporting multiclock probabilistic analysis. Chen et al. [36] translated multiclock requirement modelling with CCSL into NuSMV to verify its consistency.The mentioned works mainly use model transformation for the multiclock CCSL model, and part of them gives the semantic mapping rules, but most of them do not provide rigorous proof for behavior equivalence and model bisimulation. In this paragraph, we list several works considering behavior conservation through model bisimulation. Lam and Padget [37] defined syntax and semantics of UML statechart diagrams and π-calculus, translated statechart diagrams into -calculus, and adopted open bisimulation to check equivalence. Tolbi et al. [38] translated EHPNs (elementary hybrid Petri nets) into the hybrid automata model in terms of timed transition systems and gave behavior preservation proof in the form of timed bisimulation. Bodeveix et al. [39] proved the correctness of transformation AADL (Architecture and Analysis Design Language) to the target FIACRE language. Baouya et al. [40] introduced a novel verification framework translating the SysML activity diagram into the probabilistic model checker and proved the correctness and soundness of transformation. The work in [41] proposed a method to model stochastic processes with continuous states and proved the behavior equivalence based on the structural operational semantic rule. Bonchi et al. [42] introduced an enhancement up-to bisimulation technique for proving equivalence of open terms. Hülsbusch et al. [43] adopted two bisimularity preservation proof techniques and discussed the proof scalability issue. The work in [44] discussed the bisimulation approach to verify the semantic equivalence.To sum up, model transformation is an indispensable step of the model-driven development method for safety-critical software, and it is necessary to prove semantic preservation and equivalence between the source model and the terminate model. As for multiclock constraint systems, they are short of behavior reservation proof and simulation at the design stage, which is the second motivation of this work.


### 2.3. Model Verification for Multiclock Systems

According to the model-driven development approach, after model specification and model transformation, we should focus on model verification before system delivery. For three commonly used model verification methods, because theorem proving needs a lot of human interaction and formal model checking encounters the state explosion problem [45], in this paper, we adopt the model simulation method to perform model verification for multiclock constraint systems.We have carefully searched for previous work with relation to this study. Do et al. [46] provided a survey on simulation models to verify connected and automated intelligent vehicles and showed that simulation-based analysis guides performance measures. Related works in [47, 48] provided an approach for conjoint simulation to enjoy the benefit of understanding multiclock systems’ synchronization at the early design model. Mallet and De Simone [49] proposed two different techniques to perform state-based specification and conduct causal and temporal analysis in the simulation engine. Morando et al. [50] adopted a simulation-based approach using the traffic microsimulator surrogate safety assessment model and suggested that autonomous vehicles can improve traffic safety significantly. Shen et al. [51] proposed an early potential warning system to guide driving behaviors and verified reliability by means of cosimulation. Luo et al. [52] presented an approach to enhance traffic safety through rear-end collision models and numerical simulation. The work in [53] proposed a predictive control model for multivehicle lane-change cooperative maneuver to improve safety of intelligent traffic.In conclusion, as for multiclock constraint and safety-critical autonomous systems, software concepts, assumptions, and terminologies may be inconsistent because of the limitation of real data. The emergent autonomous systems are composed of multiple clocks, events, and entities which benefit from agent-based modelling and simulations [54], and simulation results provide guidance to identify and avoid potential deadlocks, errors, and hazards as early as possible in the design phase, which is another motivation for our work.


## 2.1. System Modelling and Model Transformation

Autonomous driving system is a kind of multiclock constraint system, so we should provide rigorous modelling methods to ensure safety and correctness. Firstly, we discuss relevant work involving system modelling and model transformation. Bochmann et al. [16] presented the controller synthesis and compositional verification for multilane traffic maneuvers. Arcile et al. [17] proposed a framework using timed automata and model checker UPPAAL (developed by Uppsala University and Aalborg University) to verify safety and robustness properties. Kamali et al. [18] constructed a spatial controller using hybrid agent architecture to model autonomous lane-change maneuvers for real-time and spatial properties. Webster et al. [19] introduced an approach combining formal verification and flight simulation for autonomous unmanned aircraft. Akhtar and Missen [20] demonstrated a method to construct a stepwise refinement multiagent model using process algebra from abstract to concrete concepts incrementally and showed how to ensure the safety and liveness properties for concurrent and interacting cooperative autonomous systems. The work in [21] introduced an abstract model for autonomous urban traffic scenarios using multilane spatial logic and showed that controllers modelled by extended timed automata can be proved safe using spatial reasoning at intersections. The aforementioned papers mainly use formal modelling methods directly at the beginning of requirement engineering. However, semiformal modelling can bridge the gap between natural requirements and formal models.Now, we will briefly discuss the relationships between our work and existing work about modelling of cooperative autonomous systems. Bernardi et al. [22] extended the UML profile, which can specialize for the railway domain and then used model transformation to generate repairable fault tree and Bayesian network models. Kapos et al. [23] explored a declarative approach and converted query/view/transformation-relation SysML model to executable simulation models, fully conforming model-driven architecture concepts. Caltais et al. [24] wanted to link two worlds of modelling and formal verification through providing transformation rules from SysML to Promela and prove the correctness based on ATL- (Atlas Transformation Language-) based transformation. Dickerson et al. [25] proposed a transformation metamodel between the UML activity model and fault tree model for end-to-end safe development process. Alshboul and Petriu [26] proposed an approach to automatically transform SysML into fault tree implemented in ETL (Epsilon Transformation Language), which can realize the purpose to integrate safety analysis within the system development process. Dias et al. [27] translated software architecture description language based on SysML and specialized profiles to process calculus CSP (communicating sequential process), and the translation can guarantee safety and liveness properties. The aforementioned works show the latest trend of model-based system development modelling and SysML model transformation for software-intensive systems. However, there is still lack of research on model transformation methods for multiclock systems, and we should provide cooperative autonomous system modelling profile and focus on transformation mapping rules for multiclock constraint time-critical systems, which is the first motivation of our work.


## 2.2. Multiclock System Specification and Semantic Equivalence

After the natural language requirement model is conducted, developers need to verify correctness and confirm whether it meets the customers’ expectations. In this section, we review existing works about multiclock specification and semantic equivalence.Multiclock timing behavior is critical for real-time cyber-physical systems. In order to analyze them early in the design stage, Goknil et al. [28] proposed a method that makes model transformation twice for formal model checking using model checker UPPAAL. The work in [29, 30] presented an approach mapping CCSL to timed input/output automata to verify safety-critical properties. The work in [31] proposed a method to combine synchronous specification language Esterel to perform validation through observers executing CCSL specification. [32–34] extended CCSL with the stochastic semantics and translated it into UPPAAL models to perform formal verification for verifying stochastic and dynamic behaviors. The work in [35] translated probabilistic CCSL into proof objective models for supporting multiclock probabilistic analysis. Chen et al. [36] translated multiclock requirement modelling with CCSL into NuSMV to verify its consistency.The mentioned works mainly use model transformation for the multiclock CCSL model, and part of them gives the semantic mapping rules, but most of them do not provide rigorous proof for behavior equivalence and model bisimulation. In this paragraph, we list several works considering behavior conservation through model bisimulation. Lam and Padget [37] defined syntax and semantics of UML statechart diagrams and π-calculus, translated statechart diagrams into -calculus, and adopted open bisimulation to check equivalence. Tolbi et al. [38] translated EHPNs (elementary hybrid Petri nets) into the hybrid automata model in terms of timed transition systems and gave behavior preservation proof in the form of timed bisimulation. Bodeveix et al. [39] proved the correctness of transformation AADL (Architecture and Analysis Design Language) to the target FIACRE language. Baouya et al. [40] introduced a novel verification framework translating the SysML activity diagram into the probabilistic model checker and proved the correctness and soundness of transformation. The work in [41] proposed a method to model stochastic processes with continuous states and proved the behavior equivalence based on the structural operational semantic rule. Bonchi et al. [42] introduced an enhancement up-to bisimulation technique for proving equivalence of open terms. Hülsbusch et al. [43] adopted two bisimularity preservation proof techniques and discussed the proof scalability issue. The work in [44] discussed the bisimulation approach to verify the semantic equivalence.To sum up, model transformation is an indispensable step of the model-driven development method for safety-critical software, and it is necessary to prove semantic preservation and equivalence between the source model and the terminate model. As for multiclock constraint systems, they are short of behavior reservation proof and simulation at the design stage, which is the second motivation of this work.


## 2.3. Model Verification for Multiclock Systems

According to the model-driven development approach, after model specification and model transformation, we should focus on model verification before system delivery. For three commonly used model verification methods, because theorem proving needs a lot of human interaction and formal model checking encounters the state explosion problem [45], in this paper, we adopt the model simulation method to perform model verification for multiclock constraint systems.We have carefully searched for previous work with relation to this study. Do et al. [46] provided a survey on simulation models to verify connected and automated intelligent vehicles and showed that simulation-based analysis guides performance measures. Related works in [47, 48] provided an approach for conjoint simulation to enjoy the benefit of understanding multiclock systems’ synchronization at the early design model. Mallet and De Simone [49] proposed two different techniques to perform state-based specification and conduct causal and temporal analysis in the simulation engine. Morando et al. [50] adopted a simulation-based approach using the traffic microsimulator surrogate safety assessment model and suggested that autonomous vehicles can improve traffic safety significantly. Shen et al. [51] proposed an early potential warning system to guide driving behaviors and verified reliability by means of cosimulation. Luo et al. [52] presented an approach to enhance traffic safety through rear-end collision models and numerical simulation. The work in [53] proposed a predictive control model for multivehicle lane-change cooperative maneuver to improve safety of intelligent traffic.In conclusion, as for multiclock constraint and safety-critical autonomous systems, software concepts, assumptions, and terminologies may be inconsistent because of the limitation of real data. The emergent autonomous systems are composed of multiple clocks, events, and entities which benefit from agent-based modelling and simulations [54], and simulation results provide guidance to identify and avoid potential deadlocks, errors, and hazards as early as possible in the design phase, which is another motivation for our work.


## 3. State of the Art for Multiclock Systems’ Specification and Verification

In this section, we mainly focus on relevant developing methods and technologies for autonomous system design and analysis.


### 3.1. Model-Driven Development and SysML/MARTE

MDD (model-driven development) is an approach for designing complex software systems, especially cyber-physical systems and autonomous software systems. According to this development method, lower-level systems’ artifacts, such as source code, are derived from high-level abstract modelling artifacts. System engineers could not only reduce time consumption through reusability and modularity for researchers and practitioners but also enhance safety and security of the whole system. MDD is based on model-driven architecture and dedicated to innovative system development.The basic idea of MDD is that everything is a model, and software developing process is driven by system modelling behavior. A model is the abstraction and representation of reality for a given purpose. Although it cannot represent all aspects of the real world, it allows us to deal with problems through avoiding the complexity and improving reusability. These different models stand for different abstract levels for system development. Model-driven developing process is presented in Figure1. At the beginning of MDD, system engineers perform requirement analysis according to systems’ requirements in the form of natural language. Next, they construct a transformation requirement model by sorting out the basic concepts and relationships among all system specifications in the process of the CIM (Computational Independent Model). Then, they transform the CIM into the transformation design model belonging to the PIM (Platform-Independent Model) through M2M (Model-to-Model) transformation, which can transform the source model into another object model [55, 56]. PIM considers logical data that can be abstracted nothing to do with any application platforms. We obtain a platform-specific model (PSM) by adding concrete and related platform information in the PIM. Through the subsequent M2M transformation, PIM can be transformed into PSM. Finally, source code (or other code-related software artifacts) is obtained through Model-to-Text transformation. In the process of PIM-to-PSM transformation, metamodel and profile support different abstraction model construction, and transformation metamodel defines the abstract syntax and static semantics of the corresponding metalanguage. The profile defining the concrete syntax of the language extends a reference metamodel to adapt for specific platform, particular domain, or a software development method. The transformation model consisting of transformation rules conforms to the transformation metamodel and maps constructors from the source model to constructors of the target model, which are in conformance with the source metamodel and target metamodel, respectively. When transformation is executed, transformation function receives the source model instantiated from the PIM as the input and generates the target model instantiated from the PSM as the output.Figure 1
Modeling process and transformations in MDD.There are many languages supporting MDD, such as UML (Unified Modeling Language), SysML, CCSL, AltaRica, and AADL. SysML is a graphical modelling language based on general purpose, and it supports modelling hardware and software codesign, coping with high complexity and avoiding traditionally time-consuming development [57]. The purpose of SysML is to describe, analyze, design, and verify complex systems. CADS are a safety-critical and complex system, so it is necessary to perform formal analysis at the stage of design phase for ensuring safety of autonomous systems. One step of model transformation is needed to transform the informal or semiformal model into the formal model for rigorous and comprehensive analysis. A model transformation is similar to a program responsible for transforming one representation into another. Main M2M transformation approaches include relational/declarative, imperative/operational, graph-based, and hybrid. This work mainly pays attention to relational/declarative approaches, and transformation specification languages focus on the mapping relationship between input elements and their corresponding output elements. So, we should define the mapping relationship using mathematical specification predicates and input-output constraints [58].MARTE system (Modeling and Analysis of Real-Time and Embedded system) combines the latest research results of industry and academia in the embedded field, and it is an open and extensible modelling specification through stereotype, tagged-value, and constraint to extend SysML’s modelling capability. Its architecture can be classified into two categories dealing with quantitative and qualitative aspects, respectively, and it is composed of some subprofiles, as is shown in Figure2. It mainly contains four subextension packs, including foundations, design model, analysis model, and annexes, in the MARTE library. Time package including in MARTE foundations is the main profile for modelling real-time behaviors, which defines time structure, time access, time usage, and other necessary time modelling elements and methods. Time access defines concepts and specifications of representing time structures among these time packages related to this work, such as clock, clock type, and current time. The “foundations” package is made up of the following profiles: (1), core elements which support to model the systems’ operational modes; (2), nfp profile which provides modelling constraints for specifying, defining, and applying nonfunctional information to a SysML model; and (3), time profile which contains concepts of time structure, time access, and time usage, which are the main modelling and verifying modes for embedded real-time systems. When CCSL starts to appear, it is a textual specification and companion language complementary to the time profile allowing us to describe the clock constraints in MARTE annexes, and now, CCSL has been fully developed as an independent specification language for logical clock and chronometric clock. Then, we introduce CCSL relevant definitions and concepts and give primary syntax and semantics of the CCSL.Figure 2
View of MARTE architecture and time package.


### 3.2. Syntax and Semantics of the CCSL

Clocks in the CCSL can be seen as events, and their instants stand for event occurrences. They can be logical or physical clocks and dense or discrete clocks [48]. In this paper, we mainly consider discrete clocks. Clocks with the arrival of logical sequence describe behaviors of systems instead of arrival of physical data. In order to describe multiclock systems more conveniently, CCSL allows each clock to be defined independently and only needs to describe existing system behavior and logical restriction relationship between clocks, without assuming total reference clock of a system, which is more conducive to the flexibility of system description. CCSL can specify constraints and evolutions among clocks, which are presented in the form of clock relations or clock expressions. The clock relation may be synchronous or asynchronous, and we can use clock expression to define new clocks based on other existing clocks. The core concept of multiclock constrained language CCSL is that a logical clock consists of a series of moments (instants), a moment corresponding to a tick of the clock. Now, we elaborate on preliminary definitions.At the beginning, we give the definition of the logical clock and multiclock constraint system referring to synchronous modelling language SIGNAL [59]. Logical clock, introduced by L. Lamport, is the central concept in CCSL, which abstracts physical time to partial order of SysML events. Clock constraint system can be divided into two categories, Monoclock system and multiclock system.Definition 1 (logical clock).
In CCSL, a logical clock is a quintuple notation,Ins,<,Lab,λcl,U, which represents a set of ordered instants. Formally, a clock c=Ins,<,Lab,λcl,U, where Ins is a sequential set of instants, < is a quasi-order relation on Ins, Lab is a set of labels, λcl:Ins⟶Lab is a labeling function, and U stands for logical clock units and is often called tick abstractly. For any discrete logical clock, ci denotes ith instant in Insc, and for each ci∈tick,idle, Insc is the set of occurrences or ticks for clock c. Now, we give relevant definitions for initial and terminal instants, respectively.(1)
i∈Insc is the initial instant of clock c if and only if ∀j∈Insc/i,i,j∈<c(2)
i∈Insc is the terminal instant of clock c if and only if ∀j∈Insc/i,j,i∈<c
For any instanti∈Insc, i∘ and i∘ stand for the predecessor and successor of i in Insc, respectively. If i is neither the initial instant nor terminal instant, ∃m∈ℕ, ℕ is the set of natural numbers, which makes cm=i, then cm−1=i∘,cm+1=i∘; and if i∈Insc is the initial instant, then there is only successor instant, and there is no predecessor for i; if i∈Insc is the terminal instant, then there is only predecessor instant, and there is no successor for i. Now, we give an example for the logical clock, and the graphical representation of clock April is shown in Figure 3.
clock April=1,2,…,29,30,<,2020.4.1,2020.4.2,…,2020.4.29,2020.4.30,λ,day.(1)
<:i<j,i∈1,2,…,29∧j∈2,3,…,30∧j=i+1.(2)
λcl:Ins⟶D,∀i∈I,λcli=2020.4.i.Figure 3
Graphical representation of clock April.Definition 2.
Monoclock system and multiclock system
A monoclock system is a system in that all activations of subsystems (also called subclocks) are controlled by a single and global master clock; a multiclock system is a system composed of several functionally independent systems, in which each system holds its own activation clock, and there is no master clock existing in the whole system.
In a monoclock model, each component’s clock would have a strict dependency relationship to the system’s global master clock, which would result in tight coupling between subsystem clocks and the global clock. Once one component’s clock frequency changes, the global clock and other subclocks also need to be adjusted accordingly. Multiclock systems are globally asynchronous and locally synchronous distribute systems, which are called the formal modelling framework polychrony [60, 61]. Components contained in the multiclock system obey to multiple clock rates, it has no global clock, and each component works according to its own clock, which is loosely coupled with other clocks, and clock synchronization takes place only between components that interact. A clock in the timed automata model captures physical real-time value properties, which will be elapsed as transition execution, and all clocks evolve according to the same rate [62]. Therefore, a multiclock model is suitable for modelling distributed or highly parallel systems. In monoclock and multiclock systems, the clock mainly represents logical time properties, and graphical representation for them is shown in Figure 4.Figure 4
(a) Monoclock system and (b) multiclock system.
(a)(b)Definition 3 (clock schedule).
A schedule is a functionSched:ℕ⟶2c. Given an execution step i∈ℕ and clock schedule σ∈Sched, σ is an infinite or finite sequence σ0σ1,…,σi,…,i∈ℕ, C is a finite set of clocks, and each σi∈2c denotes a set of clocks that tick at step i. σi=∅,i=0c|c∈C∧ci=tick,i≥1.Definition 4 (clock history).
Given any scheduleσ, the clock history Hσ is a function Hσ:C×ℕ+⟶ℕ, which keeps inductive record of the number of ticks for each clock up to current time. It is defined recursively as(1)Hσc,i=j|j∈ℕ+,j≤i,c∈σj=Hσc,0=0,i=0,Hσc,i+1=Hσc,i,∀i∈ℕ,c∉σi,Hσc,i+1=Hσc,i+1,∀i∈ℕ,c∈σi.Definition 5 (CCSL specification).
A CCSL specification is an ordered pair relationSpec=C,Cons, where C is the set of logical clocks in Definition 3, and Cons is a finite set of clock constraints, which include clock relations and clock expressions. Clock relation consists of the connection of the logical clock and the binary operator and can be synchronous or asynchronous. The basic clock relation syntax is defined as follows.
Rel⩴c1≺c2|c1#c2c1⊆c2c1≡c2c1∼c2c1≼c2, where c1andc2 are any clocks belonging to the set C. The semantics of clock relations is shown in Table 1.
The semantic interpretations of clock relations are explained informally as follows: “precedence” means that each instant ofc2 can only occur after the corresponding instant of clock c1; “exclusion” means that any two clocks c1,c2 cannot happen at the same instant; “subclock” means that c1 is a subclock of its superclock c2, and every instant of clock c1 coincides synchronously with one of the instants of clock c2; when clock c1 and clock c2 satisfy c1⊆c2∧c1⊇c2, two clocks are said to be synchronous and can be denoted as c1≡c2; “causality” means that when an event causes another one, the result event cannot occur if the cause event does not happen, so every clock c1 has to precede clock c2 in the same instant in schedule σ; and “alternation” relation ∼is derived from the precedence relation ≺ shown in Table 1. ∼ is a form of bounded ≺, and clock c1 alternates with c2 which is denoted as c1∼c2 or c1≺1c2, and an instant of c1 precedes the same instant of c2 which in turn precedes the next instant of c1. A possible schedule of clock relations is shown in Figure 5. In the result of simulation of TimeSquare presence, there are two kinds of links between two different ticks: red link, which stands for coincidences (strongly synchronous) and blue arrows, which stand for causalities (weakly synchronous).
Clock constraints can either be clock relations or clock expressions. Every clock expression is a set of clock definitions, and we can use an expression to define a new clock based on a set of parameters. The basic clock expression syntax is defined as follows.
Exp⩴c1+c2c1∗c2c1$donc2c1∝pc1⊳c2|c1▶ c2|c1↯c2c1∨c2c1∧c2|c1∧n, where c1andc2 are any clocks belonging to the set C. The semantics of clock expressions is shown in Table 2.
The semantic interpretations of clock expressions shown formally in Table2 are explained in natural language informally as follows: the result of the “Union” is a clock c0 which ticks whenever either c1 or c2 ticks; “Intersection” expression defines a clock c0 which ticks whenever both c1 and c2 tick at the same instant; expression “DelayFor” defines a clock c0 which is synchronous with part of the delay clock c2, and every tick of the base clock c1 starts up the counter d which will be decreased with every tick of the delay clock c2; when the counter d reaches 1, the clock c0 will occur along with the delay clock c2 at the same time; “PeriodicOn” defines a clock c0 which ticks periodically every pth tick of another base clock c1; “Sample” produces the fastest clock c0 slower than c1 that is a subclock of base clock c2, and it is synchronous with the base clock c2; it is easy to show that c0⊆c2∧c1≼c0; “StrictSample” defines a clock c0 that satisfies the formula c0⊆c2∧c1≺c0; “Supremum (Infimum)” defines the slowest (fastest) clock c0 which is faster (slower) than both clocks c1 and c2; “Preemption (UpTo)” produces a resulting clock c0 ticking in coincidence with the clock c1 and dying as soon as the clock c2 starts to tick; and “Wait” defines a clock c0 which will tick only once nth for the corresponding base clock c1, and then the resulting clock dies forever. A possible schedule of clock expressions shown in Table 2 is presented in Figure 6.Table 1
The semantics of clock relations.
Relation nameNotationKind of relationSemantics of relationsPrecedencec1≺c2Asynchronous∀i∈ℕ+,Hσc1,i=0∧Hσc2,i=0∨Hσc1,i>Hσc2,iExclusionc1#c2Asynchronous∀i∈ℕ+,c1∉σi∨c2∉σiSubclockc1⊆c2Synchronous∀i∈ℕ+,c1∈σi⟶c2∈σiCoincidencec1≡c2Synchronous∀i∈ℕ+,c1∈σi=c2∈σiCausalityc1 ≼ c2Asynchronous∀i∈ℕ+,Hσc1,i≥Hσc2,iAlternationc1∼c2Asynchronous∀i∈ℕ,c1i≺c2i∧c2i≺c1i+1Figure 5
A possible schedule of clock relations: (a)c1≺c2, (b) c1#c2, (c) c1⊆c2, (d) c1≡c2, (e) c1 ≼ c2, and (f) c1∼c2.
(a)(b)(c)(d)(e)(f)Table 2
The semantics of clock expressions.
Clock expression nameNotationKind of expressionSemantics of expressionsUnionc0≜c1+c2Synchronous∀i∈ℕ,c0∈σi⟺c1∈σi∨c2∈σiIntersectionc0≜c1∗c2Synchronous∀i∈ℕ,c0∈σi⟺c1∈σi∧c2∈σiDelayForc0≜c1$donc2Synchronous or asynchronous∃i∈ℕ,c0∈σi⟺c2∈σi∧∃j≤i,c1∈σj∧Hσc2,i−Hσc1,j=dPeriodicOnc0≜c1∝pSynchronous or asynchronous∀i∈ℕ,c0∈σi⟺Hσc1,i=p∗Hσc0,i∧c1∈σiSamplec0≜c1⊳c2Synchronous or asynchronous∀i∈ℕ,c0∈σi⟺c2∈σi∧∃0<j≤i∀j≤k<i⋅c1∈σj∧c2∉σkStrictSamplec0≜c1▶c2Synchronous or asynchronous∀i∈ℕ,c0∈σi⟺c2∈σi∧∃0<j<i∀j≤k<i⋅c1∈σj∧c2∉σkSupremumc0≜c1∨c2Synchronous or asynchronous∀i∈ℕ,Hσc0,i=minHσc1,i,Hσc2,iInfimumc0≜c1∧c2Synchronous or asynchronous∀i∈ℕ,Hσc0,i=maxHσc1,i,Hσc2,iPreemption (UpTo)c0≜c1↯c2Synchronous∀i∈ℕ,c0∈σi⟺c1∈σi∧∀0<j≤i,c2∉σjWaitc0≜c1n∧Synchronousc0∈σn∧∀i∈ℕ,i>n,c1∉σiFigure 6
A possible schedule of base clock expressions: (a)c0≜c1+c2, (b) c0≜c1∗c2, (c) c0≜c1$donc2,d=2, (d) c0≜c1∝p,p=3, (e) c0≜c1⊳c2, (f) c0≜c1▶c2, (g) c0≜c1∨c2, (h) c0≜c1∧c2, (i) c0≜c1↯c2, and (j) c0≜c1∧n,n=6.
(a)(b)(c)(d)(e)(f)(g)(h)(i)(j)


### 3.3. Model Verification and TimeSquare

After the system model is built according to the model-driven development method, one of real problems is that we need to perform model validation and verification to ensure correctness and safety of the whole system. There are various techniques used to perform model validation and verification, such as formal model checking, theorem proving, abstract interpretation, simulation, and emulation. Among these model verification techniques, simulation models are comparatively flexible to find unexpected problems at the system design phase and can be modified to accommodate changing environment to a real situation. In this paper, we focus on model simulation after constructing a conceptual model. TimeSquare is an Eclipse and model-driven software environment to cope with the MARTE time model and CCSL. This Eclipse plugin can be used to perform interactive clock-related specification, check clock constraints, and give a waveform solution [47].CCSL has rigorously formal semantics making CCSL multiclock constraint specification executable in TimeSquare. According to Definition4 (clock history), we call Hσc,i a configuration of clock c at instant i. So, a configuration is a set of enabled clocks (ticking) at a given step. At each step, the result of TimeSquare consists of a Boolean solution and a set of all valid configurations. If the polychromous clock constraint is deterministic, it will produce only one valid configuration; if it is nondeterministic, one of the possible configurations will be chosen in accordance with the solution policy, which is offered by TimeSquare among several simulation policies. When the clock specification is correct, TimeSquare will generate a valid sequence of steps, and this means that there exists a trace to satisfy clock constraints. If deadlocks are found by the solver after a finite sequence of steps in the waveforms, inconsistent specification should exist in clock constraints. The resulting traces are shown in the VCD (Value Change Dump) format, which is an IEEE standard format used by logic simulation tools. The relations between clocks provided in the TimeSquare tool are partial-order traces, and this illustrates that clocks (events) satisfy constraint specifications during simulation, early design validation, and verification.


### 3.4. Motivating Scenario: The Architecture of CADS

An autonomous car can be considered as a computer-aided and computer-controlled vehicle which monitors, percepts surroundings, guides itself, makes decisions, and is fully controlled and operated without any human interactions [63]. In fact, CADS are a kind of intelligent systems, such as reactive systems, self-adaptive systems, cyber-physical systems, and ubiquitous intelligent operating systems. These types of systems have a common characteristic that requires constant interaction with the environment continuously, but the main difference and advantage of the autonomous system are that it can “see” or percept the environment, “hear” or communicate with surroundings, and react fast enough and control independently without humans or other individual intervention. The purpose of autonomous driving system emergence is to improve driving safety, reduce environmental pollution, and ease the traffic congestion situation, but if these systems only act autonomously and lack connectivity and cooperativeness, autonomous driving systems may lead to collision, chaos, and collapse in the case of high densities and large-scale situation. Therefore, autonomous driving system must be designed not only to be interconnected but also to be cooperative. In this paper, we only consider connected and cooperative autonomous driving system because this kind of system can negotiate with other infrastructures and vehicles to share common information for safety and driving comfort level.CADS can communicate with other vehicles and infrastructures to obtain environment information; the system reacts fast enough to produce corresponding outputs. The system must cope with input events and output events, and inputs must precede outputs strictly. Events can be seen as multiclocks, and consumed time of computations and communications can be abstracted as instantaneous. Every computation time can be treated as an instant rather than a time interval; in other words, we can abstract and assume that each calculation time is zero, and meanwhile, the sequence of events (or clocks) must satisfy functional specification. This kind of model is a synchronous model. It is a type of PIM, which does not care about calculation time but only focuses on the sequence of the input event. So, synchronous model for real-time systems only cares about system functional properties and provides a high-level abstract model for system modelling and verification. In order to introduce the process of specification and simulation for CADS, we should present the architecture and basic elements in the autonomous driving system. SysML profile for the CADS architecture model and knowledge model is designed and shown in Figure7. In the design stage of system development, it is necessary to model structural and behavioral aspects in autonomous systems.Figure 7
SysML profile for autonomous driving system architecture.The architecture model contains all blocks and functional operations regarding the user, environment, and autonomous vehicles. Model safety is found on the basis of formal description. The detailed definition is as follows.Definition 6.
The autonomous architecture model (AAM) is a quadruple notationAAM⩴BA,RA,EA,CA:(1)
BA refers to the finite set of autonomous system blocks and is constructed based on the extended BDD (Block Definition Diagram) stereotype. BA can be expressed as(2)BA=Perception,Understanding,Planner,Actuator,User,Environment,KnowledgeBase.(2)
RA refers to the finite set of autonomous system relationships, which represent connections between functional blocks. RA can be expressed as RA⊆BA×BA,RA=monitor,trigger,precedence,stimulus,response,invoke, which is used to describe the interaction between autonomous software blocks, and its semantic interpretation is shown in Table 3.(3)
EA refers to the function of autonomous system operation OA⊆BA·OA evolution, which stands for each functional block operation type. Different blocks have different functional operations and belong to their own operation subset which is related to the corresponding attributes and will evolve when activities of operation occur. EA:BA×RA⟶BA stands for the state transition; as for any operation BA·OA, when it occurs and satisfies transition conditions, the system will evolve to the next state. For example, if the vehicle’s operations occur in block perception, such as Vehicle-to-Vehicle (V2V), Vehicle-to-Infrastructure (V2I), and other perceive actions through sensor tools (Lidar, Radar, Cameras, VisualSensors, etc.), for perceiving TrafficSnapshot (OccupyLane, ClaimLane, Position, Speed, Acceleration, and SafetyDistance), the operations (Observe, DataProcess, and Conform) will be triggered according to TrafficRule and PrioriInformation.(4)
CA refers to the finite set of conditions, which defines constraint information in the process of autonomous software execution. As for the <<stereotype>> Knowledge Base, SA=Invariant,Precondition,Postcondition.Table 3
Semantic interpretation of relationship in autonomous software.
RelationSemanticsInterpretation of relation semanticsMonitorA⟶MBRepresents the relation of monitor;A will periodically monitor B’sB′s operation status and dataTriggerA⟶CBIf the conditionC in block A is satisfied, the operation in block B will be executedPrecedenceA;BAfter the operations in blockA are completed, operations in block B will be executed successivelyStimulusA;Bc1‖Cc2As for blockA and the relevant conditions c1 and c2, if c1c2 is satisfied, the operations in block BC will be executedResponseA⟶RBBlockA will adjust the parameters, behaviors, and structures of block B according to the corresponding policiesInvokeA⟶IBRepresents the relation of invoke; blockB stores the model and data needed for implementation of A


## 3.1. Model-Driven Development and SysML/MARTE

MDD (model-driven development) is an approach for designing complex software systems, especially cyber-physical systems and autonomous software systems. According to this development method, lower-level systems’ artifacts, such as source code, are derived from high-level abstract modelling artifacts. System engineers could not only reduce time consumption through reusability and modularity for researchers and practitioners but also enhance safety and security of the whole system. MDD is based on model-driven architecture and dedicated to innovative system development.The basic idea of MDD is that everything is a model, and software developing process is driven by system modelling behavior. A model is the abstraction and representation of reality for a given purpose. Although it cannot represent all aspects of the real world, it allows us to deal with problems through avoiding the complexity and improving reusability. These different models stand for different abstract levels for system development. Model-driven developing process is presented in Figure1. At the beginning of MDD, system engineers perform requirement analysis according to systems’ requirements in the form of natural language. Next, they construct a transformation requirement model by sorting out the basic concepts and relationships among all system specifications in the process of the CIM (Computational Independent Model). Then, they transform the CIM into the transformation design model belonging to the PIM (Platform-Independent Model) through M2M (Model-to-Model) transformation, which can transform the source model into another object model [55, 56]. PIM considers logical data that can be abstracted nothing to do with any application platforms. We obtain a platform-specific model (PSM) by adding concrete and related platform information in the PIM. Through the subsequent M2M transformation, PIM can be transformed into PSM. Finally, source code (or other code-related software artifacts) is obtained through Model-to-Text transformation. In the process of PIM-to-PSM transformation, metamodel and profile support different abstraction model construction, and transformation metamodel defines the abstract syntax and static semantics of the corresponding metalanguage. The profile defining the concrete syntax of the language extends a reference metamodel to adapt for specific platform, particular domain, or a software development method. The transformation model consisting of transformation rules conforms to the transformation metamodel and maps constructors from the source model to constructors of the target model, which are in conformance with the source metamodel and target metamodel, respectively. When transformation is executed, transformation function receives the source model instantiated from the PIM as the input and generates the target model instantiated from the PSM as the output.Figure 1
Modeling process and transformations in MDD.There are many languages supporting MDD, such as UML (Unified Modeling Language), SysML, CCSL, AltaRica, and AADL. SysML is a graphical modelling language based on general purpose, and it supports modelling hardware and software codesign, coping with high complexity and avoiding traditionally time-consuming development [57]. The purpose of SysML is to describe, analyze, design, and verify complex systems. CADS are a safety-critical and complex system, so it is necessary to perform formal analysis at the stage of design phase for ensuring safety of autonomous systems. One step of model transformation is needed to transform the informal or semiformal model into the formal model for rigorous and comprehensive analysis. A model transformation is similar to a program responsible for transforming one representation into another. Main M2M transformation approaches include relational/declarative, imperative/operational, graph-based, and hybrid. This work mainly pays attention to relational/declarative approaches, and transformation specification languages focus on the mapping relationship between input elements and their corresponding output elements. So, we should define the mapping relationship using mathematical specification predicates and input-output constraints [58].MARTE system (Modeling and Analysis of Real-Time and Embedded system) combines the latest research results of industry and academia in the embedded field, and it is an open and extensible modelling specification through stereotype, tagged-value, and constraint to extend SysML’s modelling capability. Its architecture can be classified into two categories dealing with quantitative and qualitative aspects, respectively, and it is composed of some subprofiles, as is shown in Figure2. It mainly contains four subextension packs, including foundations, design model, analysis model, and annexes, in the MARTE library. Time package including in MARTE foundations is the main profile for modelling real-time behaviors, which defines time structure, time access, time usage, and other necessary time modelling elements and methods. Time access defines concepts and specifications of representing time structures among these time packages related to this work, such as clock, clock type, and current time. The “foundations” package is made up of the following profiles: (1), core elements which support to model the systems’ operational modes; (2), nfp profile which provides modelling constraints for specifying, defining, and applying nonfunctional information to a SysML model; and (3), time profile which contains concepts of time structure, time access, and time usage, which are the main modelling and verifying modes for embedded real-time systems. When CCSL starts to appear, it is a textual specification and companion language complementary to the time profile allowing us to describe the clock constraints in MARTE annexes, and now, CCSL has been fully developed as an independent specification language for logical clock and chronometric clock. Then, we introduce CCSL relevant definitions and concepts and give primary syntax and semantics of the CCSL.Figure 2
View of MARTE architecture and time package.


## 3.2. Syntax and Semantics of the CCSL

Clocks in the CCSL can be seen as events, and their instants stand for event occurrences. They can be logical or physical clocks and dense or discrete clocks [48]. In this paper, we mainly consider discrete clocks. Clocks with the arrival of logical sequence describe behaviors of systems instead of arrival of physical data. In order to describe multiclock systems more conveniently, CCSL allows each clock to be defined independently and only needs to describe existing system behavior and logical restriction relationship between clocks, without assuming total reference clock of a system, which is more conducive to the flexibility of system description. CCSL can specify constraints and evolutions among clocks, which are presented in the form of clock relations or clock expressions. The clock relation may be synchronous or asynchronous, and we can use clock expression to define new clocks based on other existing clocks. The core concept of multiclock constrained language CCSL is that a logical clock consists of a series of moments (instants), a moment corresponding to a tick of the clock. Now, we elaborate on preliminary definitions.At the beginning, we give the definition of the logical clock and multiclock constraint system referring to synchronous modelling language SIGNAL [59]. Logical clock, introduced by L. Lamport, is the central concept in CCSL, which abstracts physical time to partial order of SysML events. Clock constraint system can be divided into two categories, Monoclock system and multiclock system.Definition 1 (logical clock).
In CCSL, a logical clock is a quintuple notation,Ins,<,Lab,λcl,U, which represents a set of ordered instants. Formally, a clock c=Ins,<,Lab,λcl,U, where Ins is a sequential set of instants, < is a quasi-order relation on Ins, Lab is a set of labels, λcl:Ins⟶Lab is a labeling function, and U stands for logical clock units and is often called tick abstractly. For any discrete logical clock, ci denotes ith instant in Insc, and for each ci∈tick,idle, Insc is the set of occurrences or ticks for clock c. Now, we give relevant definitions for initial and terminal instants, respectively.(1)
i∈Insc is the initial instant of clock c if and only if ∀j∈Insc/i,i,j∈<c(2)
i∈Insc is the terminal instant of clock c if and only if ∀j∈Insc/i,j,i∈<c
For any instanti∈Insc, i∘ and i∘ stand for the predecessor and successor of i in Insc, respectively. If i is neither the initial instant nor terminal instant, ∃m∈ℕ, ℕ is the set of natural numbers, which makes cm=i, then cm−1=i∘,cm+1=i∘; and if i∈Insc is the initial instant, then there is only successor instant, and there is no predecessor for i; if i∈Insc is the terminal instant, then there is only predecessor instant, and there is no successor for i. Now, we give an example for the logical clock, and the graphical representation of clock April is shown in Figure 3.
clock April=1,2,…,29,30,<,2020.4.1,2020.4.2,…,2020.4.29,2020.4.30,λ,day.(1)
<:i<j,i∈1,2,…,29∧j∈2,3,…,30∧j=i+1.(2)
λcl:Ins⟶D,∀i∈I,λcli=2020.4.i.Figure 3
Graphical representation of clock April.Definition 2.
Monoclock system and multiclock system
A monoclock system is a system in that all activations of subsystems (also called subclocks) are controlled by a single and global master clock; a multiclock system is a system composed of several functionally independent systems, in which each system holds its own activation clock, and there is no master clock existing in the whole system.
In a monoclock model, each component’s clock would have a strict dependency relationship to the system’s global master clock, which would result in tight coupling between subsystem clocks and the global clock. Once one component’s clock frequency changes, the global clock and other subclocks also need to be adjusted accordingly. Multiclock systems are globally asynchronous and locally synchronous distribute systems, which are called the formal modelling framework polychrony [60, 61]. Components contained in the multiclock system obey to multiple clock rates, it has no global clock, and each component works according to its own clock, which is loosely coupled with other clocks, and clock synchronization takes place only between components that interact. A clock in the timed automata model captures physical real-time value properties, which will be elapsed as transition execution, and all clocks evolve according to the same rate [62]. Therefore, a multiclock model is suitable for modelling distributed or highly parallel systems. In monoclock and multiclock systems, the clock mainly represents logical time properties, and graphical representation for them is shown in Figure 4.Figure 4
(a) Monoclock system and (b) multiclock system.
(a)(b)Definition 3 (clock schedule).
A schedule is a functionSched:ℕ⟶2c. Given an execution step i∈ℕ and clock schedule σ∈Sched, σ is an infinite or finite sequence σ0σ1,…,σi,…,i∈ℕ, C is a finite set of clocks, and each σi∈2c denotes a set of clocks that tick at step i. σi=∅,i=0c|c∈C∧ci=tick,i≥1.Definition 4 (clock history).
Given any scheduleσ, the clock history Hσ is a function Hσ:C×ℕ+⟶ℕ, which keeps inductive record of the number of ticks for each clock up to current time. It is defined recursively as(1)Hσc,i=j|j∈ℕ+,j≤i,c∈σj=Hσc,0=0,i=0,Hσc,i+1=Hσc,i,∀i∈ℕ,c∉σi,Hσc,i+1=Hσc,i+1,∀i∈ℕ,c∈σi.Definition 5 (CCSL specification).
A CCSL specification is an ordered pair relationSpec=C,Cons, where C is the set of logical clocks in Definition 3, and Cons is a finite set of clock constraints, which include clock relations and clock expressions. Clock relation consists of the connection of the logical clock and the binary operator and can be synchronous or asynchronous. The basic clock relation syntax is defined as follows.
Rel⩴c1≺c2|c1#c2c1⊆c2c1≡c2c1∼c2c1≼c2, where c1andc2 are any clocks belonging to the set C. The semantics of clock relations is shown in Table 1.
The semantic interpretations of clock relations are explained informally as follows: “precedence” means that each instant ofc2 can only occur after the corresponding instant of clock c1; “exclusion” means that any two clocks c1,c2 cannot happen at the same instant; “subclock” means that c1 is a subclock of its superclock c2, and every instant of clock c1 coincides synchronously with one of the instants of clock c2; when clock c1 and clock c2 satisfy c1⊆c2∧c1⊇c2, two clocks are said to be synchronous and can be denoted as c1≡c2; “causality” means that when an event causes another one, the result event cannot occur if the cause event does not happen, so every clock c1 has to precede clock c2 in the same instant in schedule σ; and “alternation” relation ∼is derived from the precedence relation ≺ shown in Table 1. ∼ is a form of bounded ≺, and clock c1 alternates with c2 which is denoted as c1∼c2 or c1≺1c2, and an instant of c1 precedes the same instant of c2 which in turn precedes the next instant of c1. A possible schedule of clock relations is shown in Figure 5. In the result of simulation of TimeSquare presence, there are two kinds of links between two different ticks: red link, which stands for coincidences (strongly synchronous) and blue arrows, which stand for causalities (weakly synchronous).
Clock constraints can either be clock relations or clock expressions. Every clock expression is a set of clock definitions, and we can use an expression to define a new clock based on a set of parameters. The basic clock expression syntax is defined as follows.
Exp⩴c1+c2c1∗c2c1$donc2c1∝pc1⊳c2|c1▶ c2|c1↯c2c1∨c2c1∧c2|c1∧n, where c1andc2 are any clocks belonging to the set C. The semantics of clock expressions is shown in Table 2.
The semantic interpretations of clock expressions shown formally in Table2 are explained in natural language informally as follows: the result of the “Union” is a clock c0 which ticks whenever either c1 or c2 ticks; “Intersection” expression defines a clock c0 which ticks whenever both c1 and c2 tick at the same instant; expression “DelayFor” defines a clock c0 which is synchronous with part of the delay clock c2, and every tick of the base clock c1 starts up the counter d which will be decreased with every tick of the delay clock c2; when the counter d reaches 1, the clock c0 will occur along with the delay clock c2 at the same time; “PeriodicOn” defines a clock c0 which ticks periodically every pth tick of another base clock c1; “Sample” produces the fastest clock c0 slower than c1 that is a subclock of base clock c2, and it is synchronous with the base clock c2; it is easy to show that c0⊆c2∧c1≼c0; “StrictSample” defines a clock c0 that satisfies the formula c0⊆c2∧c1≺c0; “Supremum (Infimum)” defines the slowest (fastest) clock c0 which is faster (slower) than both clocks c1 and c2; “Preemption (UpTo)” produces a resulting clock c0 ticking in coincidence with the clock c1 and dying as soon as the clock c2 starts to tick; and “Wait” defines a clock c0 which will tick only once nth for the corresponding base clock c1, and then the resulting clock dies forever. A possible schedule of clock expressions shown in Table 2 is presented in Figure 6.Table 1
The semantics of clock relations.
Relation nameNotationKind of relationSemantics of relationsPrecedencec1≺c2Asynchronous∀i∈ℕ+,Hσc1,i=0∧Hσc2,i=0∨Hσc1,i>Hσc2,iExclusionc1#c2Asynchronous∀i∈ℕ+,c1∉σi∨c2∉σiSubclockc1⊆c2Synchronous∀i∈ℕ+,c1∈σi⟶c2∈σiCoincidencec1≡c2Synchronous∀i∈ℕ+,c1∈σi=c2∈σiCausalityc1 ≼ c2Asynchronous∀i∈ℕ+,Hσc1,i≥Hσc2,iAlternationc1∼c2Asynchronous∀i∈ℕ,c1i≺c2i∧c2i≺c1i+1Figure 5
A possible schedule of clock relations: (a)c1≺c2, (b) c1#c2, (c) c1⊆c2, (d) c1≡c2, (e) c1 ≼ c2, and (f) c1∼c2.
(a)(b)(c)(d)(e)(f)Table 2
The semantics of clock expressions.
Clock expression nameNotationKind of expressionSemantics of expressionsUnionc0≜c1+c2Synchronous∀i∈ℕ,c0∈σi⟺c1∈σi∨c2∈σiIntersectionc0≜c1∗c2Synchronous∀i∈ℕ,c0∈σi⟺c1∈σi∧c2∈σiDelayForc0≜c1$donc2Synchronous or asynchronous∃i∈ℕ,c0∈σi⟺c2∈σi∧∃j≤i,c1∈σj∧Hσc2,i−Hσc1,j=dPeriodicOnc0≜c1∝pSynchronous or asynchronous∀i∈ℕ,c0∈σi⟺Hσc1,i=p∗Hσc0,i∧c1∈σiSamplec0≜c1⊳c2Synchronous or asynchronous∀i∈ℕ,c0∈σi⟺c2∈σi∧∃0<j≤i∀j≤k<i⋅c1∈σj∧c2∉σkStrictSamplec0≜c1▶c2Synchronous or asynchronous∀i∈ℕ,c0∈σi⟺c2∈σi∧∃0<j<i∀j≤k<i⋅c1∈σj∧c2∉σkSupremumc0≜c1∨c2Synchronous or asynchronous∀i∈ℕ,Hσc0,i=minHσc1,i,Hσc2,iInfimumc0≜c1∧c2Synchronous or asynchronous∀i∈ℕ,Hσc0,i=maxHσc1,i,Hσc2,iPreemption (UpTo)c0≜c1↯c2Synchronous∀i∈ℕ,c0∈σi⟺c1∈σi∧∀0<j≤i,c2∉σjWaitc0≜c1n∧Synchronousc0∈σn∧∀i∈ℕ,i>n,c1∉σiFigure 6
A possible schedule of base clock expressions: (a)c0≜c1+c2, (b) c0≜c1∗c2, (c) c0≜c1$donc2,d=2, (d) c0≜c1∝p,p=3, (e) c0≜c1⊳c2, (f) c0≜c1▶c2, (g) c0≜c1∨c2, (h) c0≜c1∧c2, (i) c0≜c1↯c2, and (j) c0≜c1∧n,n=6.
(a)(b)(c)(d)(e)(f)(g)(h)(i)(j)


## 3.3. Model Verification and TimeSquare

After the system model is built according to the model-driven development method, one of real problems is that we need to perform model validation and verification to ensure correctness and safety of the whole system. There are various techniques used to perform model validation and verification, such as formal model checking, theorem proving, abstract interpretation, simulation, and emulation. Among these model verification techniques, simulation models are comparatively flexible to find unexpected problems at the system design phase and can be modified to accommodate changing environment to a real situation. In this paper, we focus on model simulation after constructing a conceptual model. TimeSquare is an Eclipse and model-driven software environment to cope with the MARTE time model and CCSL. This Eclipse plugin can be used to perform interactive clock-related specification, check clock constraints, and give a waveform solution [47].CCSL has rigorously formal semantics making CCSL multiclock constraint specification executable in TimeSquare. According to Definition4 (clock history), we call Hσc,i a configuration of clock c at instant i. So, a configuration is a set of enabled clocks (ticking) at a given step. At each step, the result of TimeSquare consists of a Boolean solution and a set of all valid configurations. If the polychromous clock constraint is deterministic, it will produce only one valid configuration; if it is nondeterministic, one of the possible configurations will be chosen in accordance with the solution policy, which is offered by TimeSquare among several simulation policies. When the clock specification is correct, TimeSquare will generate a valid sequence of steps, and this means that there exists a trace to satisfy clock constraints. If deadlocks are found by the solver after a finite sequence of steps in the waveforms, inconsistent specification should exist in clock constraints. The resulting traces are shown in the VCD (Value Change Dump) format, which is an IEEE standard format used by logic simulation tools. The relations between clocks provided in the TimeSquare tool are partial-order traces, and this illustrates that clocks (events) satisfy constraint specifications during simulation, early design validation, and verification.


## 3.4. Motivating Scenario: The Architecture of CADS

An autonomous car can be considered as a computer-aided and computer-controlled vehicle which monitors, percepts surroundings, guides itself, makes decisions, and is fully controlled and operated without any human interactions [63]. In fact, CADS are a kind of intelligent systems, such as reactive systems, self-adaptive systems, cyber-physical systems, and ubiquitous intelligent operating systems. These types of systems have a common characteristic that requires constant interaction with the environment continuously, but the main difference and advantage of the autonomous system are that it can “see” or percept the environment, “hear” or communicate with surroundings, and react fast enough and control independently without humans or other individual intervention. The purpose of autonomous driving system emergence is to improve driving safety, reduce environmental pollution, and ease the traffic congestion situation, but if these systems only act autonomously and lack connectivity and cooperativeness, autonomous driving systems may lead to collision, chaos, and collapse in the case of high densities and large-scale situation. Therefore, autonomous driving system must be designed not only to be interconnected but also to be cooperative. In this paper, we only consider connected and cooperative autonomous driving system because this kind of system can negotiate with other infrastructures and vehicles to share common information for safety and driving comfort level.CADS can communicate with other vehicles and infrastructures to obtain environment information; the system reacts fast enough to produce corresponding outputs. The system must cope with input events and output events, and inputs must precede outputs strictly. Events can be seen as multiclocks, and consumed time of computations and communications can be abstracted as instantaneous. Every computation time can be treated as an instant rather than a time interval; in other words, we can abstract and assume that each calculation time is zero, and meanwhile, the sequence of events (or clocks) must satisfy functional specification. This kind of model is a synchronous model. It is a type of PIM, which does not care about calculation time but only focuses on the sequence of the input event. So, synchronous model for real-time systems only cares about system functional properties and provides a high-level abstract model for system modelling and verification. In order to introduce the process of specification and simulation for CADS, we should present the architecture and basic elements in the autonomous driving system. SysML profile for the CADS architecture model and knowledge model is designed and shown in Figure7. In the design stage of system development, it is necessary to model structural and behavioral aspects in autonomous systems.Figure 7
SysML profile for autonomous driving system architecture.The architecture model contains all blocks and functional operations regarding the user, environment, and autonomous vehicles. Model safety is found on the basis of formal description. The detailed definition is as follows.Definition 6.
The autonomous architecture model (AAM) is a quadruple notationAAM⩴BA,RA,EA,CA:(1)
BA refers to the finite set of autonomous system blocks and is constructed based on the extended BDD (Block Definition Diagram) stereotype. BA can be expressed as(2)BA=Perception,Understanding,Planner,Actuator,User,Environment,KnowledgeBase.(2)
RA refers to the finite set of autonomous system relationships, which represent connections between functional blocks. RA can be expressed as RA⊆BA×BA,RA=monitor,trigger,precedence,stimulus,response,invoke, which is used to describe the interaction between autonomous software blocks, and its semantic interpretation is shown in Table 3.(3)
EA refers to the function of autonomous system operation OA⊆BA·OA evolution, which stands for each functional block operation type. Different blocks have different functional operations and belong to their own operation subset which is related to the corresponding attributes and will evolve when activities of operation occur. EA:BA×RA⟶BA stands for the state transition; as for any operation BA·OA, when it occurs and satisfies transition conditions, the system will evolve to the next state. For example, if the vehicle’s operations occur in block perception, such as Vehicle-to-Vehicle (V2V), Vehicle-to-Infrastructure (V2I), and other perceive actions through sensor tools (Lidar, Radar, Cameras, VisualSensors, etc.), for perceiving TrafficSnapshot (OccupyLane, ClaimLane, Position, Speed, Acceleration, and SafetyDistance), the operations (Observe, DataProcess, and Conform) will be triggered according to TrafficRule and PrioriInformation.(4)
CA refers to the finite set of conditions, which defines constraint information in the process of autonomous software execution. As for the <<stereotype>> Knowledge Base, SA=Invariant,Precondition,Postcondition.Table 3
Semantic interpretation of relationship in autonomous software.
RelationSemanticsInterpretation of relation semanticsMonitorA⟶MBRepresents the relation of monitor;A will periodically monitor B’sB′s operation status and dataTriggerA⟶CBIf the conditionC in block A is satisfied, the operation in block B will be executedPrecedenceA;BAfter the operations in blockA are completed, operations in block B will be executed successivelyStimulusA;Bc1‖Cc2As for blockA and the relevant conditions c1 and c2, if c1c2 is satisfied, the operations in block BC will be executedResponseA⟶RBBlockA will adjust the parameters, behaviors, and structures of block B according to the corresponding policiesInvokeA⟶IBRepresents the relation of invoke; blockB stores the model and data needed for implementation of A


## 4. Proposed Methodology in This Paper

In practice of model-driven software development, it is increasingly clear that indispensable design and analysis processes should be integrated together. Design model using design language should be converted into the analysis model using analysis language in order to perform model verification and analysis on the transformed analysis model for safety. Model transformation technology is used to perform this conversion, and transformation process should preserve behavior semantics of the source design model. In this section, we propose an approach to transform the design model into the analysis model and then verify semantic equivalence for this conversion through the model bisimulation proof. First of all, SMD (state machine diagram) for CADS is introduced in the following section.


### 4.1. Syntax and Semantics of SMD for CADS

In the previousSection 3.4, we use the SysML BDD structure diagram to obtain static specification for the CADS scenario. BDD depicts classes of the major components, attributes, corresponding operations, and relationship between them. In order to ease comprehension of CADS behavior and analyze simulation execution traces, we should construct SysML dynamic diagrams to specify interactive behavior between the system and the surrounding environment and then perform model transformation for the formal model to verify and validate safety properties. SMD is constructed from states and transitions and is very convenient for clearly describing the dynamic behavior transition and state changes in the system. A state is denoted as a rounded rectangle, whereas transitions are arrows from one state to another labelled with three optional parts: a trigger event, a guard condition, and an effect (a sequence of actions) [27]. Now, we present the main features of the state machine for CADS to show system reactive behaviors.First of all, we can define SMD as this 6-tupleSMD⩴S,S0,E,G,Act,Tr.


#### 4.1.1. Vertices and Transitions

A vertex is a node in SMD, which may stand for a state, a final state, or a pseudo-state. A transition refers to a directed labelled edge connecting a source vertex and the corresponding target vertex. A transition may be a compound transition which is composed of multiple transitions connected via fork, junction, or join pseudo-state. LetTr be a set of transitions; we can use the following notation for Tr: tr:sv⟶eg/atv, and for a transition tr and a set of vertices V, sv∈Vand tv∈V are the source and target vertex of the corresponding transition tr; e∈E,g∈G,a∈Act are the trigger event, guard condition, and effective behaviors associated with tr, respectively. The semantics of transition function tr is that if the trigger event occurs and Boolean guard conditions are satisfied, then the sequence actions would be executed, and the system translates from the current state into the successive state. Especially, trigger events can be classified into external environmental events and internal state events due to autonomous systems’ new features. Through this distinction, autonomous systems can percept the external trigger event, such as weather condition, traffic sign, traffic code, road conditions, and surrounding sensors’ input data.


#### 4.1.2. Regions

A region is the container of vertices and transitions and indicates orthogonal parts which may be a composite state or a substate machine. Figure8 contains an orthogonal substate machine region s5:ClaimLane.Figure 8
SMD for the autonomous overtaking system.


#### 4.1.3. States

There are three types of states:type:S⟶simple,region,composite. Simple state, e.g., in Figure 8, (s1:TurnLeft) is not further refined; region state, e.g., in Figure 8, (s5:ClaimLane) is composed of at least two orthogonal states; composite state indicates that the state can be further refined. Each state may have an optional action associated with it: entry, exit, and activity. We can use the type function to avoid unnecessary redundancy and invalid attribute combinations. Let S be a given set of states; S0refers to the initial state in SMD and for every state s∈S satisfying the following relation.(3)types=simple iffs.issimple∧¬s.isregion∧¬s.iscomposite,region iff¬s.issimple∧s.isregion∧¬s.iscomposite,composite iff¬s.issimple∧¬s.isregion∧s.iscomposite.


#### 4.1.4. Pseudo-States

A pseudo-state is a vertex in the state machine connecting multiple transitions into more complex paths. Pseudo-states are extensions of state machine syntax in order to express rich enough behaviors. We can define a pseudo-state as a tuple:ps=r,f; r∈region defines the region to which the pseudo-state belongs; f∈S is an option recording the last active state field and is only used in shallow history or deep history pseudo-state conditions. There are approximately ten kinds of pseudo-states defined in SysML SMD:(4)ps=initial,exitpoint,choice,join,fork,junction,terminate,entrypoint,shallowhistory,deephistory..Then, we define SOS (structured operational semantics) of SMD for CADS using LTS (labelled transition system). The definition of LTS is shown as follows.Definition 7.
A LTS is a 6-tupleLTS⩴S,Act,⟶,Init,AP,L such thatS is a set of states (the state space).Act is the set of actions.⟶⊆S×Act×Sis a relation of the transition. We can denote the transition s,α,s′∈⟶ as a short notation s⟶αs′.Init⊆S is a set of initial states.AP is a set of atomic propositions.L:S⟶2AP is a labeling function.
LTS is often drawn as a directed graph with vertices representing the states and edges representing the transitions. Now, we give an example combining CADS in Figure8.


#### 4.1.5. LTS Example

Consider a part of the CADS model; at the beginning of overtaking, we care about the transition betweens1:TurnLeft and s2:OvertakeReq.LTSC=SC,ActC,⟶C,InitC,APC,LC, where(5)SC=s1,s2;ActC=SendReq,waiting;⟶C=s1,SendReq,s2,s2,waiting,s1;APC=Creq≤4s;LC=s1⟶∅,s2⟶Creq≤4s.According to Definition7, we give the formal and precise SOS rules for SMD.Definition 8.
Operation semantics of sequence rule
Given source and target states, trigger event, Boolean guard condition, and sequence effect action satisfy thatss,st⊆S,e∈E,g∈G,anda∈Act, if the trigger event occurs and Boolean condition is true, then ss⟶eg/ast.


#### 4.1.6. Sequence Example

At this point, we give the sequence operation semantics shown in Figure8. From source state s7:OverTaking to s8:TurnRight, Boolean guard conditions should be satisfied, and action Acceleration should be performed.(6)PositionOvertaker−PositionOvertakee≥SafeDistance andCot>10s.Definition 9.
Operation semantics of choice rule
Choice operation semantics is defined as a functionchoice⟶ss×e×gi×a×st,ss,st∈S∧ei∈E∧gi∈G∧ai∈Act∧i∈ℕ, where guards G and actions Act are environment signatures for choice rules, guards G are conditions of the transition to happen and can be represented as formulas in some logical language, and actions Act are operations of the block diagram or assignments of attributes.
The choice SOS is defined as follows:(7)ss1⟶e1g1/a1st1,ss1⟶e2g2/a2st2,…,ss1⟶eigi/aisti,…ss1⟶∑i∈ℕeigi/∑i∈ℕaisti.


#### 4.1.7. Choice Example

According to Figure8, there exist four choice transitions, and we choose ss=s5,st=s5ors6 to explain choice operation semantics. When event and condition e1=WithdrawOvertaking∧g1=NoCollision==No are satisfied, the transition s5⟶s5 will occur. When another event and guard condition e2=Overtaking∧g2=NoCollision==Yes∧a2=Steering are satisfied, the transition s5⟶s6 will occur.Definition 10.
Operation semantics of fork rule
A fork vertex splits the incoming transition into two or more terminating transitions belonging to orthogonal target vertices. We can define the fork operation semantics as follows:fork⟶ss×e×g×a×r1.s1int|r2.s2int|…|rn.snint; rn.snint,n∈ℕ, indicates that target states in fork behavior belong to the orthogonal region. Every transition behaves independently, currently, and synchronously. Now, the definition of fork operation semantics is as follows:(8)ss⟶eg/ar1.s1int,ss⟶eg/ar2.s2int,…,ss⟶eg/arn.snintss⟶eg/ar1.s1intr2.s2int…|rn.snint.


#### 4.1.8. Fork Example

Referring to Figure8, after the ego vehicle receives agreement information during the invariant Creq≤4s, the state will translate into two orthogonal fork states s5.s1intands5.s2int belonging to the composite state s5:ClaimLane.Definition 11.
Operation semantics of join rule
A join vertex merges more than one transition emanating from source vertices belonging to different orthogonal regions and results in synchronous execution. We can define join operation semantics as follows:(9)join⟶r1.s1finr2.s2fin…|rn.snfin×e×g×a×st,where rn.snfin,n∈ℕ, indicates that source states in join behavior belong to the orthogonal region. Source states are from independent, current, and synchronously occurring regions. Now, the definition of join operation semantics is as follows:(10)r1.s1fin⟶eg/ast,r2.s2fin⟶eg/ast,…,rn.snfin⟶eg/astr1.s1finr2.s2fin…|rn.snfin⟶eg/ast.


#### 4.1.9. Join Example

Referring to Figure8, the first region r1 of s5:ClaimLaneis responsible for ego_front_vehicle’s collision checking, while the second region r2 of s5:ClaimLaneis responsible for ego_behind_vehicle’s collision checking. The join state in Figure 8 is a choice Pseudo-state from two orthogonal regions r1 and r2.According to natural language description for autonomous overtaking requirements, we can derive SMD in a semiformal way to specify multiclock system constraints, as shown in Figure8.


### 4.2. Semantics of CCSL and Model Transformation

However, due to the lack of precisely formal semantics, UML SMD suffers from an incessant criticism and should manage the gap between the system specification and the design model validation and eliminate ambiguity. In this section, we transform the design model into the analysis model for further verification. In order to do correct model transformation, first of all, we give the SOS for the formal analysis model. Referring toSection 3, now we give simple Backus–Naur form for CCSL syntax, which contains CC (clock constraint), CR (clock relation), CE (clock expression), CS (clock specification), and Rop (relation operators).(11)<CC>⩴<CC>,<CR>CR<CR>if bool<CR>⩴<CS><Rop><CS><Rop>⩴<subclock>exclusion<coincidence>|precedence<CS>⩴<clock>|<CE><CE>⩴bool?<CE>:<CE><clock>!1|!0|<CE><await>natural|CE><sample><CE|<CE><s_sample><CE>|CE><upto><CE|CE><concat><CE|CE><union><CE|<CE><inter><CE>|CE><defer><CE|CE><sup><CE|CE><inf><CE.According to the simple syntax, we give operation semantics in terms of LTS for the formal modelling language CCSL. Based on Definition7 LTS, we focus on source and target states of a transition; so, the corresponding transition functions are added: α,β:Tr⟶S; Tr denotes a set of transitions, S denotes a set of states, and α,β denote the source and target state of a transition, respectively. The function λ:Tr⟶Act is added to denote the action which is responsible for the corresponding transition. When clock constraints are treated as transition systems and put in parallel, their composition can be defined as a synchronized product of labelled transition systems.Definition 12.
(synchronized product). Givenn automata Au and are based on LTSs in Definition 7, Au=Au1,Au2,Au3,…,Aun; let a synchronization constraint SC be a subset of the product Au1×Au2×⋯×Aun,SC⊆Au1×Au2×⋯×Aun, and synchronization constraints are beneficial for capturing semantics of CCSL multiclock operators. For the LTS Aui=Si,Acti,Tri,Initi,APi,Li and αiTri⊆Si,βiTri⊆Si, synchronized product Γi of Aui over the set SC is defined as follows:(12)S=S1×S2×⋯×Sn,Init=Init1×Init2×⋯×Initn,Tr=tr1,tr2,…,trn∈Tr1×Tr2×⋯×Trn|λ1tr1,λ2tr2,…,λntrn∈SC,λtr1,tr2,…,trn=λ1tr1,λ2tr2,…,λntrn.
For the clockci∈C involved in the automaton execution, function Tri⟶tick,idleC defines each transition to associate clock states with the corresponding CCSL operators. Based on the actually ticked clocks, the states update according to the function Si⟶TriP, which will return outgoing transitions for a state.


#### 4.2.1. Example of SOS of Clock Relation

According to the definition of synchronization constraintSC and synchronized product Γi, operational semantics of multiclock relations is as follows:(1)
Subclock relationc1⊆c2 is the synchronized product clock c1,c2 and SCS=c1,c2,ϕ,c2,ϕ,ϕ.(2)
Coincidence relationc1≡c2 is the synchronized product clock c1,c2 and SCCO=c1,c2,ϕ,ϕ.(3)
Exclusion relationc1#c2 is the synchronized product clock c1,c2 and SCE=c1,ϕ,ϕ,c2,ϕ,ϕ.(4)
Precedence relationc1≺c2 is the synchronized product clock c1,c2 and SCP=c1,ϕ∧c1,c2∧ϕ,c2∧c1,ϕ>c1,c2∨c1,ϕ∨c1,c2∨ϕ,ϕ.(5)
Causality relationc1≼c2 is the synchronized product clock c1,c2 and SCCA=c1,ϕ,c1,c2,ϕ,ϕ.(6)
Union expressionc0≜c1+c2 is represented by the synchronized product clock c1,c2 and SCU=c1,c2,c0,c1,ϕ,c0,ϕ,c2,c0ϕ,ϕ,ϕ.(7)
Intersection expressionc0≜c1∗c2 is represented by the synchronized product clock c1,c2 and(13)SCI=c1,c2,c0,c1,ϕ,ϕ,ϕ,c2,ϕϕ,ϕ,ϕ.With respect to other clock relations and clock expressions, we can give operation semantics based on state-based LTS. Then, we introduce how to transform the formalized design SMD model into analysis and formal CCSL models and prove that the bisimulation relation is preserved and satisfied in the process of model transformation.Rule 1:∀ssmd∈Ssmd⇒ssmd⟶sccsl∧sccsl∈Sccsl: for every state ssmd belonging to the SMD, it will be mapped to a state sccsl belonging to the state-based CCSL model.Rule 2:∀e∈Esmd⇒e⟶c∧c∈λtr,tr∈Trccsl: for every trigger event e in the state machine, it will be mapped to a clock in the target state-based CCSL model.Rule 3:∀g∈Gsmd⟹g⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl: for every guard condition belonging to the state machine, it will be mapped to the Boolean condition in the choice expression in the state-based CCSL transition system.Rule 4: operation semantics of sequence rule transformation:(14)∀s1,s2∈Ssmd,e∈Esmd,g∈Gsmd,s1,e,g,s2∈Trsmd⇒s1⟶s1′,s2⟶s2′,s1′,s2′∈Sccsl,e⟶c,c∈λtr,tr∈Trccsl,g⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl.As for the sequence operation, state, event, and guard of the state machine can be transformed into state, clock, and choice Boolean condition in the state-based CCSL model, respectively.Rule 5: operation semantics of choice rule transformation:(15)∀Ss,Tri,ei,gi,S1,Tri∈Ssmd∧i∈ℕ∧ei∈E∧gi∈G∧Ss,ei,gi,Tri∈Trsmd⇒Ss⟶S∧Tri⟶CR.choice∧S,CR.choice∈Sccsl∧i∈ℕ∧ei⟶ci,ci∈λtr,tr∈Trccsl∧gi⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl∧S,CR.choice,ci,Trchoice.Bool∈Trccsl.As for one source state in the state machine, there are two or more uncertain target states, which can be transformed into the CCSL model using the clock structure choice operator.Rule 6: operation semantics of fork rule transformation:(16)ss⟶eg/ar1.s1intr2.s2int⋯|rn.snint,n∈ℕ,ss,r1,2,…,n,s1int,2int,…,nint∈Ssmd,e∈E,g∈G,a∈Act⇒ss′⟶ctr1′|tr2′|⋯|trn′,n∈ℕ,ss′,tr1,2,…,n′∈Sccsl,c∈λtr,tr∈Trccsl.The operation semantics of fork behavior is from one state to more than one state. This is concurrent and independent relation. In the process of fork transformation, concurrent behaviors in state machine orthogonal regions can be mapped to the clock coincidence relation in the CCSL time structure.Rule 7; operation semantics of join rule transformation:(17)r1.s1fin,r2.s2fin,…,rn.snfin⟶eg/ast,n∈ℕ,r1,2,…,n,s1fin,2fin,…,nfin,st∈Ssmd,e∈E,g∈G,a∈Act⇒s1′s2′…|sn′⟶cst,n∈ℕ,s1,2,…,n′,st∈Sccsl,c∈λtr,tr∈Trccsl.The operation semantics of join behavior is from more than one transition emanating from source vertices belonging to different orthogonal regions to one synchronous target state. In the process of join transformation, the number of more than one concurrent source state can be mapped to the DelayForc0≜c1$donc2 clock expression behaviors.


### 4.3. Proof of Bisimulation Equivalence

After introducing the syntax and semantics of modelling language and performing model transformation, behavioral preservation or trace execution equivalence should be proved. If two transition systems perform the same sequences of actions from initial states, respectively, we treat them as equivalent execution models. There are two necessary and important reasons to compare semantics of two systems through bisimulation: one reason is that if two systems satisfy bisimulation equivalence, we could not distinguish them by behavioral observation. Another reason is that if two systems or processes are bisimulation equivalent, then transitions in the first system can be done and finished in the second system. We note that two systems can simulate each other. We give the definition of bisimulation and proof in Definition13.Definition 13.
(bisimulation). Let two labelled transition systemsLTS1=Q1,Act,⟶,Init1,AP1,L1,LTS2=Q2,Act,⟶,Init2,AP2,L2 and a relation R⊆Q1×Q2 between the two labelled transition systems be a bisimulation relation, iff for all q1∈Q1,q2∈Q2 such that q1Rq2 holds; it also holds for all actions α∈Act that(1)
Wheneverq1⟶αq1′, then for some q2′,q2⟶αq2′andq1′Rq2′(2)
Wheneverq2⟶αq2′, then for some q1′,q1⟶αq1′andq1′Rq2′
If two transition systems satisfy the bisimulation definition, we sayLTS1 and LTS2are bisimular LTS1≈RbsimLTS2, and there exists a bisimulation relation Rbsim (denoted as ≈) between them. When the relation LTS1≈LTS2 holds, we can draw the following conclusion that all traces of LTS1 can also be preserved in another transition system LTS2 and vice versa. Accordingly, the relation LTS1≈LTS2 indicates that LTS1 preserves all possible behaviors of another transition system LTS2.Theorem 1.
LTS1 of SMD SSMD and LTS2 of CCSL SCCSL satisfy bisimulation relation, SSMD≈SCCSL.Proof.
LetSSMD=Q1,Act,TrS,Init1,AP1,L1 be the LTS of SMD and SCCSL=Q2,Act,TrC,Init2,AP2,L2 be the LTS of CCSL. Let R be a binary relation on Q1×Q2,R⊆Q1×Q2. As for q1,q1′∈Q1,α∈Act,TrSq1,α=q1′q1⟶αq1′;q2,q2′∈Q2,α∈Act,TrCq2,α=q2′q2⟶αq2′, whenever q1Rq2forq1,q2∈R, next we should check the following assertions:(1)
∀αAct,q1′∈Q1. If q1⟶αq1′, then there is q2′∈Q2 such that q2⟶αq2′ with q1′Rq2′.(2)
∀α∈Act,q2′∈Q2. If q2⟶αq2′, then there is q1′∈Q1 such that q1⟶αq1′ with q1′Rq2′.
Given two behavior preservation transformation transition systemsSSMD and SCCSL,(1.1) If∃e∈Act,q1′∈Q1,trS=q1×e×q1′∈TrS, according to Definition 12 and transformation rules, λq1′=e′|e′∈e∘ (i∘ and i∘ stand for the predecessor and successor of the ith occurrence in clock C). So, in the model SSMD, events e,e′satisfye≺e′, and so, in the SCCSL model, there exists a transition trC=q2×e×q2′∈TrC, and q2′=e′|e≺e′; so, we can come to the following conclusion: λ1q1′=λ2q2′,q1′,q2′∈R.(1.2) If∃e∈Act,q2′∈Q2,trC=q2×e×q2′∈TrC, according to Definition 12 and transformation rules, λq2′=e′|e′∈e∘. So, in the model SCCSL, events e,e′satisfye≺e′, and so, in the SSMD model, there exists a transition tS=q1×e×q1′∈TS, and q1′=e′|e≺e′; so, we can come to the following conclusion: λ2q2′=λ1q1′,q1′,q2′∈R.(1.3) If there exists a sequence of events, such ase,e′∈Eseq, ∃e∈Act,q1′∈Q1,trS=q1×e,e′×q1′∈TrS, according to Definition 12 and transformation rules, λq1′=e″|e″∈e∘∪e′∘. So, in the model SSMD, events satisfy the relation e″≺eore″≺e′, and so, in the SCCSL model, there exists a transition trC=q2×e,e′×q2′∈TrC, and q2′=e″|e″≺e∨e″≺e′; so, we can come to the following conclusion: λ1q1′=λ2q2′,q1′,q2′∈R.(1.4) If there exists a sequence of events, such ase,e′∈Eseq, ∃e∈Act,q2′∈Q2,trC=q2×e,e′×q2′∈TrC, according to Definition 12 and transformation rules, λq2′=e″|e″∈e∘∪e′∘. So, in the model SCCSL, events satisfy the relation e″≺eore″≺e′, and so, in the SSMD model, there exists a transition trS=q1×e,e′×q1′∈TrS, and q1′=e″|e″≺e∨e″≺e′; so, we can come to the following conclusion: λ2q2′=λ1q1′,q1′,q2′∈R.
In conclusion, according to Definition13 (bisimulation) and the previous proof process, for ∀q1∈Q1,α∈Act,ifq1⟶αq1′,then∃q2′∈Q2q2⟶αq2′andq1′Rq2′ and ∀q2∈Q2,α∈Act,ifq2⟶αq2′,then∃q1′∈Q1q1⟶αq1′andq1′Rq2′. So, the relation R satisfies the relation bisimulation definition, and the two models satisfy bisimulation through defining formal syntax and semantics for source and termination models and model semantic mapping rules.


## 4.1. Syntax and Semantics of SMD for CADS

In the previousSection 3.4, we use the SysML BDD structure diagram to obtain static specification for the CADS scenario. BDD depicts classes of the major components, attributes, corresponding operations, and relationship between them. In order to ease comprehension of CADS behavior and analyze simulation execution traces, we should construct SysML dynamic diagrams to specify interactive behavior between the system and the surrounding environment and then perform model transformation for the formal model to verify and validate safety properties. SMD is constructed from states and transitions and is very convenient for clearly describing the dynamic behavior transition and state changes in the system. A state is denoted as a rounded rectangle, whereas transitions are arrows from one state to another labelled with three optional parts: a trigger event, a guard condition, and an effect (a sequence of actions) [27]. Now, we present the main features of the state machine for CADS to show system reactive behaviors.First of all, we can define SMD as this 6-tupleSMD⩴S,S0,E,G,Act,Tr.


### 4.1.1. Vertices and Transitions

A vertex is a node in SMD, which may stand for a state, a final state, or a pseudo-state. A transition refers to a directed labelled edge connecting a source vertex and the corresponding target vertex. A transition may be a compound transition which is composed of multiple transitions connected via fork, junction, or join pseudo-state. LetTr be a set of transitions; we can use the following notation for Tr: tr:sv⟶eg/atv, and for a transition tr and a set of vertices V, sv∈Vand tv∈V are the source and target vertex of the corresponding transition tr; e∈E,g∈G,a∈Act are the trigger event, guard condition, and effective behaviors associated with tr, respectively. The semantics of transition function tr is that if the trigger event occurs and Boolean guard conditions are satisfied, then the sequence actions would be executed, and the system translates from the current state into the successive state. Especially, trigger events can be classified into external environmental events and internal state events due to autonomous systems’ new features. Through this distinction, autonomous systems can percept the external trigger event, such as weather condition, traffic sign, traffic code, road conditions, and surrounding sensors’ input data.


### 4.1.2. Regions

A region is the container of vertices and transitions and indicates orthogonal parts which may be a composite state or a substate machine. Figure8 contains an orthogonal substate machine region s5:ClaimLane.Figure 8
SMD for the autonomous overtaking system.


### 4.1.3. States

There are three types of states:type:S⟶simple,region,composite. Simple state, e.g., in Figure 8, (s1:TurnLeft) is not further refined; region state, e.g., in Figure 8, (s5:ClaimLane) is composed of at least two orthogonal states; composite state indicates that the state can be further refined. Each state may have an optional action associated with it: entry, exit, and activity. We can use the type function to avoid unnecessary redundancy and invalid attribute combinations. Let S be a given set of states; S0refers to the initial state in SMD and for every state s∈S satisfying the following relation.(3)types=simple iffs.issimple∧¬s.isregion∧¬s.iscomposite,region iff¬s.issimple∧s.isregion∧¬s.iscomposite,composite iff¬s.issimple∧¬s.isregion∧s.iscomposite.


### 4.1.4. Pseudo-States

A pseudo-state is a vertex in the state machine connecting multiple transitions into more complex paths. Pseudo-states are extensions of state machine syntax in order to express rich enough behaviors. We can define a pseudo-state as a tuple:ps=r,f; r∈region defines the region to which the pseudo-state belongs; f∈S is an option recording the last active state field and is only used in shallow history or deep history pseudo-state conditions. There are approximately ten kinds of pseudo-states defined in SysML SMD:(4)ps=initial,exitpoint,choice,join,fork,junction,terminate,entrypoint,shallowhistory,deephistory..Then, we define SOS (structured operational semantics) of SMD for CADS using LTS (labelled transition system). The definition of LTS is shown as follows.Definition 7.
A LTS is a 6-tupleLTS⩴S,Act,⟶,Init,AP,L such thatS is a set of states (the state space).Act is the set of actions.⟶⊆S×Act×Sis a relation of the transition. We can denote the transition s,α,s′∈⟶ as a short notation s⟶αs′.Init⊆S is a set of initial states.AP is a set of atomic propositions.L:S⟶2AP is a labeling function.
LTS is often drawn as a directed graph with vertices representing the states and edges representing the transitions. Now, we give an example combining CADS in Figure8.


### 4.1.5. LTS Example

Consider a part of the CADS model; at the beginning of overtaking, we care about the transition betweens1:TurnLeft and s2:OvertakeReq.LTSC=SC,ActC,⟶C,InitC,APC,LC, where(5)SC=s1,s2;ActC=SendReq,waiting;⟶C=s1,SendReq,s2,s2,waiting,s1;APC=Creq≤4s;LC=s1⟶∅,s2⟶Creq≤4s.According to Definition7, we give the formal and precise SOS rules for SMD.Definition 8.
Operation semantics of sequence rule
Given source and target states, trigger event, Boolean guard condition, and sequence effect action satisfy thatss,st⊆S,e∈E,g∈G,anda∈Act, if the trigger event occurs and Boolean condition is true, then ss⟶eg/ast.


### 4.1.6. Sequence Example

At this point, we give the sequence operation semantics shown in Figure8. From source state s7:OverTaking to s8:TurnRight, Boolean guard conditions should be satisfied, and action Acceleration should be performed.(6)PositionOvertaker−PositionOvertakee≥SafeDistance andCot>10s.Definition 9.
Operation semantics of choice rule
Choice operation semantics is defined as a functionchoice⟶ss×e×gi×a×st,ss,st∈S∧ei∈E∧gi∈G∧ai∈Act∧i∈ℕ, where guards G and actions Act are environment signatures for choice rules, guards G are conditions of the transition to happen and can be represented as formulas in some logical language, and actions Act are operations of the block diagram or assignments of attributes.
The choice SOS is defined as follows:(7)ss1⟶e1g1/a1st1,ss1⟶e2g2/a2st2,…,ss1⟶eigi/aisti,…ss1⟶∑i∈ℕeigi/∑i∈ℕaisti.


### 4.1.7. Choice Example

According to Figure8, there exist four choice transitions, and we choose ss=s5,st=s5ors6 to explain choice operation semantics. When event and condition e1=WithdrawOvertaking∧g1=NoCollision==No are satisfied, the transition s5⟶s5 will occur. When another event and guard condition e2=Overtaking∧g2=NoCollision==Yes∧a2=Steering are satisfied, the transition s5⟶s6 will occur.Definition 10.
Operation semantics of fork rule
A fork vertex splits the incoming transition into two or more terminating transitions belonging to orthogonal target vertices. We can define the fork operation semantics as follows:fork⟶ss×e×g×a×r1.s1int|r2.s2int|…|rn.snint; rn.snint,n∈ℕ, indicates that target states in fork behavior belong to the orthogonal region. Every transition behaves independently, currently, and synchronously. Now, the definition of fork operation semantics is as follows:(8)ss⟶eg/ar1.s1int,ss⟶eg/ar2.s2int,…,ss⟶eg/arn.snintss⟶eg/ar1.s1intr2.s2int…|rn.snint.


### 4.1.8. Fork Example

Referring to Figure8, after the ego vehicle receives agreement information during the invariant Creq≤4s, the state will translate into two orthogonal fork states s5.s1intands5.s2int belonging to the composite state s5:ClaimLane.Definition 11.
Operation semantics of join rule
A join vertex merges more than one transition emanating from source vertices belonging to different orthogonal regions and results in synchronous execution. We can define join operation semantics as follows:(9)join⟶r1.s1finr2.s2fin…|rn.snfin×e×g×a×st,where rn.snfin,n∈ℕ, indicates that source states in join behavior belong to the orthogonal region. Source states are from independent, current, and synchronously occurring regions. Now, the definition of join operation semantics is as follows:(10)r1.s1fin⟶eg/ast,r2.s2fin⟶eg/ast,…,rn.snfin⟶eg/astr1.s1finr2.s2fin…|rn.snfin⟶eg/ast.


### 4.1.9. Join Example

Referring to Figure8, the first region r1 of s5:ClaimLaneis responsible for ego_front_vehicle’s collision checking, while the second region r2 of s5:ClaimLaneis responsible for ego_behind_vehicle’s collision checking. The join state in Figure 8 is a choice Pseudo-state from two orthogonal regions r1 and r2.According to natural language description for autonomous overtaking requirements, we can derive SMD in a semiformal way to specify multiclock system constraints, as shown in Figure8.


## 4.1.1. Vertices and Transitions

A vertex is a node in SMD, which may stand for a state, a final state, or a pseudo-state. A transition refers to a directed labelled edge connecting a source vertex and the corresponding target vertex. A transition may be a compound transition which is composed of multiple transitions connected via fork, junction, or join pseudo-state. LetTr be a set of transitions; we can use the following notation for Tr: tr:sv⟶eg/atv, and for a transition tr and a set of vertices V, sv∈Vand tv∈V are the source and target vertex of the corresponding transition tr; e∈E,g∈G,a∈Act are the trigger event, guard condition, and effective behaviors associated with tr, respectively. The semantics of transition function tr is that if the trigger event occurs and Boolean guard conditions are satisfied, then the sequence actions would be executed, and the system translates from the current state into the successive state. Especially, trigger events can be classified into external environmental events and internal state events due to autonomous systems’ new features. Through this distinction, autonomous systems can percept the external trigger event, such as weather condition, traffic sign, traffic code, road conditions, and surrounding sensors’ input data.


## 4.1.2. Regions

A region is the container of vertices and transitions and indicates orthogonal parts which may be a composite state or a substate machine. Figure8 contains an orthogonal substate machine region s5:ClaimLane.Figure 8
SMD for the autonomous overtaking system.


## 4.1.3. States

There are three types of states:type:S⟶simple,region,composite. Simple state, e.g., in Figure 8, (s1:TurnLeft) is not further refined; region state, e.g., in Figure 8, (s5:ClaimLane) is composed of at least two orthogonal states; composite state indicates that the state can be further refined. Each state may have an optional action associated with it: entry, exit, and activity. We can use the type function to avoid unnecessary redundancy and invalid attribute combinations. Let S be a given set of states; S0refers to the initial state in SMD and for every state s∈S satisfying the following relation.(3)types=simple iffs.issimple∧¬s.isregion∧¬s.iscomposite,region iff¬s.issimple∧s.isregion∧¬s.iscomposite,composite iff¬s.issimple∧¬s.isregion∧s.iscomposite.


## 4.1.4. Pseudo-States

A pseudo-state is a vertex in the state machine connecting multiple transitions into more complex paths. Pseudo-states are extensions of state machine syntax in order to express rich enough behaviors. We can define a pseudo-state as a tuple:ps=r,f; r∈region defines the region to which the pseudo-state belongs; f∈S is an option recording the last active state field and is only used in shallow history or deep history pseudo-state conditions. There are approximately ten kinds of pseudo-states defined in SysML SMD:(4)ps=initial,exitpoint,choice,join,fork,junction,terminate,entrypoint,shallowhistory,deephistory..Then, we define SOS (structured operational semantics) of SMD for CADS using LTS (labelled transition system). The definition of LTS is shown as follows.Definition 7.
A LTS is a 6-tupleLTS⩴S,Act,⟶,Init,AP,L such thatS is a set of states (the state space).Act is the set of actions.⟶⊆S×Act×Sis a relation of the transition. We can denote the transition s,α,s′∈⟶ as a short notation s⟶αs′.Init⊆S is a set of initial states.AP is a set of atomic propositions.L:S⟶2AP is a labeling function.
LTS is often drawn as a directed graph with vertices representing the states and edges representing the transitions. Now, we give an example combining CADS in Figure8.


## 4.1.5. LTS Example

Consider a part of the CADS model; at the beginning of overtaking, we care about the transition betweens1:TurnLeft and s2:OvertakeReq.LTSC=SC,ActC,⟶C,InitC,APC,LC, where(5)SC=s1,s2;ActC=SendReq,waiting;⟶C=s1,SendReq,s2,s2,waiting,s1;APC=Creq≤4s;LC=s1⟶∅,s2⟶Creq≤4s.According to Definition7, we give the formal and precise SOS rules for SMD.Definition 8.
Operation semantics of sequence rule
Given source and target states, trigger event, Boolean guard condition, and sequence effect action satisfy thatss,st⊆S,e∈E,g∈G,anda∈Act, if the trigger event occurs and Boolean condition is true, then ss⟶eg/ast.


## 4.1.6. Sequence Example

At this point, we give the sequence operation semantics shown in Figure8. From source state s7:OverTaking to s8:TurnRight, Boolean guard conditions should be satisfied, and action Acceleration should be performed.(6)PositionOvertaker−PositionOvertakee≥SafeDistance andCot>10s.Definition 9.
Operation semantics of choice rule
Choice operation semantics is defined as a functionchoice⟶ss×e×gi×a×st,ss,st∈S∧ei∈E∧gi∈G∧ai∈Act∧i∈ℕ, where guards G and actions Act are environment signatures for choice rules, guards G are conditions of the transition to happen and can be represented as formulas in some logical language, and actions Act are operations of the block diagram or assignments of attributes.
The choice SOS is defined as follows:(7)ss1⟶e1g1/a1st1,ss1⟶e2g2/a2st2,…,ss1⟶eigi/aisti,…ss1⟶∑i∈ℕeigi/∑i∈ℕaisti.


## 4.1.7. Choice Example

According to Figure8, there exist four choice transitions, and we choose ss=s5,st=s5ors6 to explain choice operation semantics. When event and condition e1=WithdrawOvertaking∧g1=NoCollision==No are satisfied, the transition s5⟶s5 will occur. When another event and guard condition e2=Overtaking∧g2=NoCollision==Yes∧a2=Steering are satisfied, the transition s5⟶s6 will occur.Definition 10.
Operation semantics of fork rule
A fork vertex splits the incoming transition into two or more terminating transitions belonging to orthogonal target vertices. We can define the fork operation semantics as follows:fork⟶ss×e×g×a×r1.s1int|r2.s2int|…|rn.snint; rn.snint,n∈ℕ, indicates that target states in fork behavior belong to the orthogonal region. Every transition behaves independently, currently, and synchronously. Now, the definition of fork operation semantics is as follows:(8)ss⟶eg/ar1.s1int,ss⟶eg/ar2.s2int,…,ss⟶eg/arn.snintss⟶eg/ar1.s1intr2.s2int…|rn.snint.


## 4.1.8. Fork Example

Referring to Figure8, after the ego vehicle receives agreement information during the invariant Creq≤4s, the state will translate into two orthogonal fork states s5.s1intands5.s2int belonging to the composite state s5:ClaimLane.Definition 11.
Operation semantics of join rule
A join vertex merges more than one transition emanating from source vertices belonging to different orthogonal regions and results in synchronous execution. We can define join operation semantics as follows:(9)join⟶r1.s1finr2.s2fin…|rn.snfin×e×g×a×st,where rn.snfin,n∈ℕ, indicates that source states in join behavior belong to the orthogonal region. Source states are from independent, current, and synchronously occurring regions. Now, the definition of join operation semantics is as follows:(10)r1.s1fin⟶eg/ast,r2.s2fin⟶eg/ast,…,rn.snfin⟶eg/astr1.s1finr2.s2fin…|rn.snfin⟶eg/ast.


## 4.1.9. Join Example

Referring to Figure8, the first region r1 of s5:ClaimLaneis responsible for ego_front_vehicle’s collision checking, while the second region r2 of s5:ClaimLaneis responsible for ego_behind_vehicle’s collision checking. The join state in Figure 8 is a choice Pseudo-state from two orthogonal regions r1 and r2.According to natural language description for autonomous overtaking requirements, we can derive SMD in a semiformal way to specify multiclock system constraints, as shown in Figure8.


## 4.2. Semantics of CCSL and Model Transformation

However, due to the lack of precisely formal semantics, UML SMD suffers from an incessant criticism and should manage the gap between the system specification and the design model validation and eliminate ambiguity. In this section, we transform the design model into the analysis model for further verification. In order to do correct model transformation, first of all, we give the SOS for the formal analysis model. Referring toSection 3, now we give simple Backus–Naur form for CCSL syntax, which contains CC (clock constraint), CR (clock relation), CE (clock expression), CS (clock specification), and Rop (relation operators).(11)<CC>⩴<CC>,<CR>CR<CR>if bool<CR>⩴<CS><Rop><CS><Rop>⩴<subclock>exclusion<coincidence>|precedence<CS>⩴<clock>|<CE><CE>⩴bool?<CE>:<CE><clock>!1|!0|<CE><await>natural|CE><sample><CE|<CE><s_sample><CE>|CE><upto><CE|CE><concat><CE|CE><union><CE|<CE><inter><CE>|CE><defer><CE|CE><sup><CE|CE><inf><CE.According to the simple syntax, we give operation semantics in terms of LTS for the formal modelling language CCSL. Based on Definition7 LTS, we focus on source and target states of a transition; so, the corresponding transition functions are added: α,β:Tr⟶S; Tr denotes a set of transitions, S denotes a set of states, and α,β denote the source and target state of a transition, respectively. The function λ:Tr⟶Act is added to denote the action which is responsible for the corresponding transition. When clock constraints are treated as transition systems and put in parallel, their composition can be defined as a synchronized product of labelled transition systems.Definition 12.
(synchronized product). Givenn automata Au and are based on LTSs in Definition 7, Au=Au1,Au2,Au3,…,Aun; let a synchronization constraint SC be a subset of the product Au1×Au2×⋯×Aun,SC⊆Au1×Au2×⋯×Aun, and synchronization constraints are beneficial for capturing semantics of CCSL multiclock operators. For the LTS Aui=Si,Acti,Tri,Initi,APi,Li and αiTri⊆Si,βiTri⊆Si, synchronized product Γi of Aui over the set SC is defined as follows:(12)S=S1×S2×⋯×Sn,Init=Init1×Init2×⋯×Initn,Tr=tr1,tr2,…,trn∈Tr1×Tr2×⋯×Trn|λ1tr1,λ2tr2,…,λntrn∈SC,λtr1,tr2,…,trn=λ1tr1,λ2tr2,…,λntrn.
For the clockci∈C involved in the automaton execution, function Tri⟶tick,idleC defines each transition to associate clock states with the corresponding CCSL operators. Based on the actually ticked clocks, the states update according to the function Si⟶TriP, which will return outgoing transitions for a state.


### 4.2.1. Example of SOS of Clock Relation

According to the definition of synchronization constraintSC and synchronized product Γi, operational semantics of multiclock relations is as follows:(1)
Subclock relationc1⊆c2 is the synchronized product clock c1,c2 and SCS=c1,c2,ϕ,c2,ϕ,ϕ.(2)
Coincidence relationc1≡c2 is the synchronized product clock c1,c2 and SCCO=c1,c2,ϕ,ϕ.(3)
Exclusion relationc1#c2 is the synchronized product clock c1,c2 and SCE=c1,ϕ,ϕ,c2,ϕ,ϕ.(4)
Precedence relationc1≺c2 is the synchronized product clock c1,c2 and SCP=c1,ϕ∧c1,c2∧ϕ,c2∧c1,ϕ>c1,c2∨c1,ϕ∨c1,c2∨ϕ,ϕ.(5)
Causality relationc1≼c2 is the synchronized product clock c1,c2 and SCCA=c1,ϕ,c1,c2,ϕ,ϕ.(6)
Union expressionc0≜c1+c2 is represented by the synchronized product clock c1,c2 and SCU=c1,c2,c0,c1,ϕ,c0,ϕ,c2,c0ϕ,ϕ,ϕ.(7)
Intersection expressionc0≜c1∗c2 is represented by the synchronized product clock c1,c2 and(13)SCI=c1,c2,c0,c1,ϕ,ϕ,ϕ,c2,ϕϕ,ϕ,ϕ.With respect to other clock relations and clock expressions, we can give operation semantics based on state-based LTS. Then, we introduce how to transform the formalized design SMD model into analysis and formal CCSL models and prove that the bisimulation relation is preserved and satisfied in the process of model transformation.Rule 1:∀ssmd∈Ssmd⇒ssmd⟶sccsl∧sccsl∈Sccsl: for every state ssmd belonging to the SMD, it will be mapped to a state sccsl belonging to the state-based CCSL model.Rule 2:∀e∈Esmd⇒e⟶c∧c∈λtr,tr∈Trccsl: for every trigger event e in the state machine, it will be mapped to a clock in the target state-based CCSL model.Rule 3:∀g∈Gsmd⟹g⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl: for every guard condition belonging to the state machine, it will be mapped to the Boolean condition in the choice expression in the state-based CCSL transition system.Rule 4: operation semantics of sequence rule transformation:(14)∀s1,s2∈Ssmd,e∈Esmd,g∈Gsmd,s1,e,g,s2∈Trsmd⇒s1⟶s1′,s2⟶s2′,s1′,s2′∈Sccsl,e⟶c,c∈λtr,tr∈Trccsl,g⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl.As for the sequence operation, state, event, and guard of the state machine can be transformed into state, clock, and choice Boolean condition in the state-based CCSL model, respectively.Rule 5: operation semantics of choice rule transformation:(15)∀Ss,Tri,ei,gi,S1,Tri∈Ssmd∧i∈ℕ∧ei∈E∧gi∈G∧Ss,ei,gi,Tri∈Trsmd⇒Ss⟶S∧Tri⟶CR.choice∧S,CR.choice∈Sccsl∧i∈ℕ∧ei⟶ci,ci∈λtr,tr∈Trccsl∧gi⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl∧S,CR.choice,ci,Trchoice.Bool∈Trccsl.As for one source state in the state machine, there are two or more uncertain target states, which can be transformed into the CCSL model using the clock structure choice operator.Rule 6: operation semantics of fork rule transformation:(16)ss⟶eg/ar1.s1intr2.s2int⋯|rn.snint,n∈ℕ,ss,r1,2,…,n,s1int,2int,…,nint∈Ssmd,e∈E,g∈G,a∈Act⇒ss′⟶ctr1′|tr2′|⋯|trn′,n∈ℕ,ss′,tr1,2,…,n′∈Sccsl,c∈λtr,tr∈Trccsl.The operation semantics of fork behavior is from one state to more than one state. This is concurrent and independent relation. In the process of fork transformation, concurrent behaviors in state machine orthogonal regions can be mapped to the clock coincidence relation in the CCSL time structure.Rule 7; operation semantics of join rule transformation:(17)r1.s1fin,r2.s2fin,…,rn.snfin⟶eg/ast,n∈ℕ,r1,2,…,n,s1fin,2fin,…,nfin,st∈Ssmd,e∈E,g∈G,a∈Act⇒s1′s2′…|sn′⟶cst,n∈ℕ,s1,2,…,n′,st∈Sccsl,c∈λtr,tr∈Trccsl.The operation semantics of join behavior is from more than one transition emanating from source vertices belonging to different orthogonal regions to one synchronous target state. In the process of join transformation, the number of more than one concurrent source state can be mapped to the DelayForc0≜c1$donc2 clock expression behaviors.


## 4.2.1. Example of SOS of Clock Relation

According to the definition of synchronization constraintSC and synchronized product Γi, operational semantics of multiclock relations is as follows:(1)
Subclock relationc1⊆c2 is the synchronized product clock c1,c2 and SCS=c1,c2,ϕ,c2,ϕ,ϕ.(2)
Coincidence relationc1≡c2 is the synchronized product clock c1,c2 and SCCO=c1,c2,ϕ,ϕ.(3)
Exclusion relationc1#c2 is the synchronized product clock c1,c2 and SCE=c1,ϕ,ϕ,c2,ϕ,ϕ.(4)
Precedence relationc1≺c2 is the synchronized product clock c1,c2 and SCP=c1,ϕ∧c1,c2∧ϕ,c2∧c1,ϕ>c1,c2∨c1,ϕ∨c1,c2∨ϕ,ϕ.(5)
Causality relationc1≼c2 is the synchronized product clock c1,c2 and SCCA=c1,ϕ,c1,c2,ϕ,ϕ.(6)
Union expressionc0≜c1+c2 is represented by the synchronized product clock c1,c2 and SCU=c1,c2,c0,c1,ϕ,c0,ϕ,c2,c0ϕ,ϕ,ϕ.(7)
Intersection expressionc0≜c1∗c2 is represented by the synchronized product clock c1,c2 and(13)SCI=c1,c2,c0,c1,ϕ,ϕ,ϕ,c2,ϕϕ,ϕ,ϕ.With respect to other clock relations and clock expressions, we can give operation semantics based on state-based LTS. Then, we introduce how to transform the formalized design SMD model into analysis and formal CCSL models and prove that the bisimulation relation is preserved and satisfied in the process of model transformation.Rule 1:∀ssmd∈Ssmd⇒ssmd⟶sccsl∧sccsl∈Sccsl: for every state ssmd belonging to the SMD, it will be mapped to a state sccsl belonging to the state-based CCSL model.Rule 2:∀e∈Esmd⇒e⟶c∧c∈λtr,tr∈Trccsl: for every trigger event e in the state machine, it will be mapped to a clock in the target state-based CCSL model.Rule 3:∀g∈Gsmd⟹g⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl: for every guard condition belonging to the state machine, it will be mapped to the Boolean condition in the choice expression in the state-based CCSL transition system.Rule 4: operation semantics of sequence rule transformation:(14)∀s1,s2∈Ssmd,e∈Esmd,g∈Gsmd,s1,e,g,s2∈Trsmd⇒s1⟶s1′,s2⟶s2′,s1′,s2′∈Sccsl,e⟶c,c∈λtr,tr∈Trccsl,g⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl.As for the sequence operation, state, event, and guard of the state machine can be transformed into state, clock, and choice Boolean condition in the state-based CCSL model, respectively.Rule 5: operation semantics of choice rule transformation:(15)∀Ss,Tri,ei,gi,S1,Tri∈Ssmd∧i∈ℕ∧ei∈E∧gi∈G∧Ss,ei,gi,Tri∈Trsmd⇒Ss⟶S∧Tri⟶CR.choice∧S,CR.choice∈Sccsl∧i∈ℕ∧ei⟶ci,ci∈λtr,tr∈Trccsl∧gi⟶Trchoice.Bool∧Trchoice.BOOL∈Trccsl∧S,CR.choice,ci,Trchoice.Bool∈Trccsl.As for one source state in the state machine, there are two or more uncertain target states, which can be transformed into the CCSL model using the clock structure choice operator.Rule 6: operation semantics of fork rule transformation:(16)ss⟶eg/ar1.s1intr2.s2int⋯|rn.snint,n∈ℕ,ss,r1,2,…,n,s1int,2int,…,nint∈Ssmd,e∈E,g∈G,a∈Act⇒ss′⟶ctr1′|tr2′|⋯|trn′,n∈ℕ,ss′,tr1,2,…,n′∈Sccsl,c∈λtr,tr∈Trccsl.The operation semantics of fork behavior is from one state to more than one state. This is concurrent and independent relation. In the process of fork transformation, concurrent behaviors in state machine orthogonal regions can be mapped to the clock coincidence relation in the CCSL time structure.Rule 7; operation semantics of join rule transformation:(17)r1.s1fin,r2.s2fin,…,rn.snfin⟶eg/ast,n∈ℕ,r1,2,…,n,s1fin,2fin,…,nfin,st∈Ssmd,e∈E,g∈G,a∈Act⇒s1′s2′…|sn′⟶cst,n∈ℕ,s1,2,…,n′,st∈Sccsl,c∈λtr,tr∈Trccsl.The operation semantics of join behavior is from more than one transition emanating from source vertices belonging to different orthogonal regions to one synchronous target state. In the process of join transformation, the number of more than one concurrent source state can be mapped to the DelayForc0≜c1$donc2 clock expression behaviors.


## 4.3. Proof of Bisimulation Equivalence

After introducing the syntax and semantics of modelling language and performing model transformation, behavioral preservation or trace execution equivalence should be proved. If two transition systems perform the same sequences of actions from initial states, respectively, we treat them as equivalent execution models. There are two necessary and important reasons to compare semantics of two systems through bisimulation: one reason is that if two systems satisfy bisimulation equivalence, we could not distinguish them by behavioral observation. Another reason is that if two systems or processes are bisimulation equivalent, then transitions in the first system can be done and finished in the second system. We note that two systems can simulate each other. We give the definition of bisimulation and proof in Definition13.Definition 13.
(bisimulation). Let two labelled transition systemsLTS1=Q1,Act,⟶,Init1,AP1,L1,LTS2=Q2,Act,⟶,Init2,AP2,L2 and a relation R⊆Q1×Q2 between the two labelled transition systems be a bisimulation relation, iff for all q1∈Q1,q2∈Q2 such that q1Rq2 holds; it also holds for all actions α∈Act that(1)
Wheneverq1⟶αq1′, then for some q2′,q2⟶αq2′andq1′Rq2′(2)
Wheneverq2⟶αq2′, then for some q1′,q1⟶αq1′andq1′Rq2′
If two transition systems satisfy the bisimulation definition, we sayLTS1 and LTS2are bisimular LTS1≈RbsimLTS2, and there exists a bisimulation relation Rbsim (denoted as ≈) between them. When the relation LTS1≈LTS2 holds, we can draw the following conclusion that all traces of LTS1 can also be preserved in another transition system LTS2 and vice versa. Accordingly, the relation LTS1≈LTS2 indicates that LTS1 preserves all possible behaviors of another transition system LTS2.Theorem 1.
LTS1 of SMD SSMD and LTS2 of CCSL SCCSL satisfy bisimulation relation, SSMD≈SCCSL.Proof.
LetSSMD=Q1,Act,TrS,Init1,AP1,L1 be the LTS of SMD and SCCSL=Q2,Act,TrC,Init2,AP2,L2 be the LTS of CCSL. Let R be a binary relation on Q1×Q2,R⊆Q1×Q2. As for q1,q1′∈Q1,α∈Act,TrSq1,α=q1′q1⟶αq1′;q2,q2′∈Q2,α∈Act,TrCq2,α=q2′q2⟶αq2′, whenever q1Rq2forq1,q2∈R, next we should check the following assertions:(1)
∀αAct,q1′∈Q1. If q1⟶αq1′, then there is q2′∈Q2 such that q2⟶αq2′ with q1′Rq2′.(2)
∀α∈Act,q2′∈Q2. If q2⟶αq2′, then there is q1′∈Q1 such that q1⟶αq1′ with q1′Rq2′.
Given two behavior preservation transformation transition systemsSSMD and SCCSL,(1.1) If∃e∈Act,q1′∈Q1,trS=q1×e×q1′∈TrS, according to Definition 12 and transformation rules, λq1′=e′|e′∈e∘ (i∘ and i∘ stand for the predecessor and successor of the ith occurrence in clock C). So, in the model SSMD, events e,e′satisfye≺e′, and so, in the SCCSL model, there exists a transition trC=q2×e×q2′∈TrC, and q2′=e′|e≺e′; so, we can come to the following conclusion: λ1q1′=λ2q2′,q1′,q2′∈R.(1.2) If∃e∈Act,q2′∈Q2,trC=q2×e×q2′∈TrC, according to Definition 12 and transformation rules, λq2′=e′|e′∈e∘. So, in the model SCCSL, events e,e′satisfye≺e′, and so, in the SSMD model, there exists a transition tS=q1×e×q1′∈TS, and q1′=e′|e≺e′; so, we can come to the following conclusion: λ2q2′=λ1q1′,q1′,q2′∈R.(1.3) If there exists a sequence of events, such ase,e′∈Eseq, ∃e∈Act,q1′∈Q1,trS=q1×e,e′×q1′∈TrS, according to Definition 12 and transformation rules, λq1′=e″|e″∈e∘∪e′∘. So, in the model SSMD, events satisfy the relation e″≺eore″≺e′, and so, in the SCCSL model, there exists a transition trC=q2×e,e′×q2′∈TrC, and q2′=e″|e″≺e∨e″≺e′; so, we can come to the following conclusion: λ1q1′=λ2q2′,q1′,q2′∈R.(1.4) If there exists a sequence of events, such ase,e′∈Eseq, ∃e∈Act,q2′∈Q2,trC=q2×e,e′×q2′∈TrC, according to Definition 12 and transformation rules, λq2′=e″|e″∈e∘∪e′∘. So, in the model SCCSL, events satisfy the relation e″≺eore″≺e′, and so, in the SSMD model, there exists a transition trS=q1×e,e′×q1′∈TrS, and q1′=e″|e″≺e∨e″≺e′; so, we can come to the following conclusion: λ2q2′=λ1q1′,q1′,q2′∈R.
In conclusion, according to Definition13 (bisimulation) and the previous proof process, for ∀q1∈Q1,α∈Act,ifq1⟶αq1′,then∃q2′∈Q2q2⟶αq2′andq1′Rq2′ and ∀q2∈Q2,α∈Act,ifq2⟶αq2′,then∃q1′∈Q1q1⟶αq1′andq1′Rq2′. So, the relation R satisfies the relation bisimulation definition, and the two models satisfy bisimulation through defining formal syntax and semantics for source and termination models and model semantic mapping rules.


## 5. Case Study

### 5.1. Autonomous Overtaking Requirement Description for CADS

Although fully autonomous road vehicles (highway, urban traffic, and country roads) without human help/interruption remain futuristic, the automobile industries have been striving to meet these expectations. Academia and industry are committed to improve safety, reliability, and traffic efficiency and ease increasingly congested traffic situations. It is especially imperative for cooperative vehicles’ lane-changing and overtaking autonomously in the multilane highway. In this paper, we focus on autonomous driving behavior due to independent and self-sufficient decision-making function. These vehicles can communicate with surrounding relevant vehicles and the infrastructure to perceive traffic information. After understanding these environment perceptions, CADS generate negotiation maneuvers for autonomous lane-changing and overtaking behaviors. Each vehicle involving coordination observes its surrounding traffic and conforms to the generating decision-making to realize overtaking autonomously. In the following, requirements about lane-changing judgement, overtaking procedures, and message exchanging for autonomous overtaking are explained.We assume that there are three one-way lanes in this paper considering the situation shown in Figure9; the first lane is reserved_lane (lane 2 in Figure 9) occupied by ego_vehicle, the second lane is applying_lane (lane 3 in Figure 9) claimed to overtake by ego_vehicle, and the third lane is the right side of adjacent_lanes (lane 1 in Figure 9). According to the traffic code, we assume that ego_vehicle must claim the left-side adjacent_lane to complete the overtaking action driving on the right-hand side of the road. In the view of the ego_vehicle overtaking scenario, the following vehicles may be involved, and there may be exist three vehicles (ego_vehicle A, ego_front_vehicle B, and ego_behind_vehicle C) in the currently reserved_lane, two vehicles (applying_lane_behind_vehicle D and applying_lane_front_vehicle E) in the applying_lane, and one vehicle (adjacent_lane_vehicle F) in the adjacent_lane. When ego_vehicle on the currently occupied road has intention to overtake, the first is to turn on the left-turn signal to remind surrounding view vehicles of the lane-change intention. At this moment, there are three safety-critical matters to confirm; firstly, CADS should confirm whether vehicles in the applying_lane are within a safe distance; secondly, after the lane-change signal is observed by them, ego_behind_vehicle within the view cannot accelerate; and the third thing is to send an overtaking message to ego_front_vehicle in the same reserved_lane. After confirmation of overtaking in the first step, overtaking negotiation stage is followed. Ego_front_vehicle needs to reply agree or disagree within a certain time (response time, we assume 4 seconds) after receiving the overtaking message. If ego_vehicle cannot receive the reply message from ego_front_vehicle exceeding response time or receives the disagree message, it should not implement lane-changing overtaking behavior and need to keep the previous driving state. If safety distance constraints are not satisfied, overtaking cannot be implemented too. Only when two constraints (receiving agree message and safety distance) are satisfied at the same time, ego_vehicle can start to perform the first lane-changing action. Overtaking behavior can be decomposed into two-times lane-change actions. After the first lane-change mentioned above, ego_vehicle should speed up, and ego_front_vehicle replying agree message just now cannot accelerate. When ego_vehicle’s spatial position is greater than ego_front_vehicle and, meanwhile, they meet safety distance for the second lane-change action, ego_vehicle can implement the second lane-change. Time interval between two-times lane-changing must not exceed stipulated overtaking_time, such as 10 seconds. After ego_vehicle completes lane-change twice and overtakes ego_front_vehicle, CADS will automatically adjust speed and maintain a safety distance between them.Figure 9
View of the ego-vehicle overtaking.


### 5.2. CCSL for Autonomous Overtaking System (AOS) Specification

In order to present the multiclock autonomous overtaking system specification, we should show involved clocks during the overtaking process. For specifying convenience, each clock’s abbreviation is given. Next, we need to list various clocks: ego_turn_signal: ets, applying_lane_safedistance: asd, ego_behind_no_acceleration: ebna, ego_send_lanechange: esl, ego_front_agree: efa, ego_front_disagree: efd, ego_no_overtaking: eno, ego_front_no_acceleration: efna, and ego_send_overtaken: eso. The functional and timing properties of the AOS are specified as follows:AOS1: ego_turn_signal is always followed by applying_lane_safedistance and ego_behind_no_acceleration, so the corresponding CCSL constraint is thatets∼asd∗ebna.AOS2: applying_lane_safedistance and ego_behind_no_acceleration trigger (cause) event ego_send_lanechange. In other words, the slowest clockasd∨ebna is faster than both clocks asd and ebna, and the tick of clock asd∨ebna can trigger the occurrence of clock esl. The corresponding CCSL constraint is that asd∨ebna≼esl.AOS3: ego_front_agree or ego_front_disagree will occur after ego_send_lanechange within a response time of 4 s. The corresponding CCSL constraint is thatesl≺efa+efddelayedFor1onc1where clockc1=IdealClk discretized By4s.AOS4: when ego_vehicle receives the reply ego_front_disagree, it must trigger the event ego_no_overtaking simultaneously, and the CCSL constraint is thatefd≡eno.AOS5: clocks efa, asd, and efna satisfy the constraintsefa∨asd≡efna, which indicates that the slowest event between receiving ego_front_agree message and satisfying applying_lane_safedistance is faster than both of mentioned events, and ego_front_vehicle should trigger the event ego_front_no_acceleration simultaneously.AOS6: the event ego_send_overtaken will occur with 10 s after the event ego_front_agree. The corresponding CCSL constraint is that(18)efa≺eso delayed For1onc2where clockc2=IdealClk discretized By10s.


### 5.3. Model Validation through Model Simulation and Analysis for the AOS

After the multiclock AOS specification, we can perform model validation through clock constraint simulation intuitively. In the previous part, we present multiclock constraint AOS formal specifications by CCSL, and in this section, clock constraint checking results of model simulation are analyzed using the special tool TimeSquare, which yields a satisfying partial-order execution trace for multiclock constraints. The yielding traces are indicated as VCD format waveforms. When multiclock constraints are correct, TimeSquare will generate a valid simulation trace, but if CCSL specifications do not satisfy all clock constraints or have conflicts, the tool cannot execute and will result in a deadlock shown as the end of VCD waveform. One of the simulation traces is partially shown in Figure10. The blue and dashed arrows stand for the precedence clock relation, whereas red and vertical solid lines stand for the coincidence relation between two synchronous instants.Figure 10
One partial simulation trace for the autonomous overtaking system.Corresponding to safety-critical system properties, clock ego_turn_signal ets must happen alternatively with the intersection clock c30 of two clocks asd and ebna. The clock constraint simulation execution results are shown in Figure10, and CCSL specification and corresponding expressions in simulation tool TimeSquare are shown in Table 4. Clock constraint ets∼asd∗ebnais satisfied, and this safety-critical property is valid. We define the slowest clock c3 which is faster than clocks asd and ebna, and the tick of supremum clock c3 will cause the tick of clock esl; the result of this clock constraint is satisfied and shown as the clock waveform. Other functional properties are also satisfied and shown in the TimeSquare yielding trace; firstly, the clock efna will only tick if the slowest definition clock csup which is faster than clocks asd and efa is ticking synchronously. Secondly, another strictly synchronous clock constraint efd≡eno describes two events occurring in coincidence; event ego_front_disagree corresponding to clock efd means another event ego_vehicle cannot change the lane and implements overtaking behavior corresponding to clock eno; similarly, if ego_front_vehicle replies agreement, then it should not accelerate at the same time. As for timing nonfunctional properties, we combine coincidence and precedence mixed constraints. The clock specification cupp1=efa≺eso delayed For1onc2where clockc2=IdealClk discretized Byd3 constraints cupp1 to tick synchronously with d3th tick of clock eso, which follows a tick of clock efa, and cupp1 is a mixed constraint since eso and efa are asynchronous precedence clock relation in Table 1. It is similar to another DelayFor constraint cupp=esl≺efa+efddelayedFor1onc1where clockc1=IdealClk discretized Byd2, so the first time interval between sending and replying communicating message and the second time interval consumed during the process of overtaking are satisfied in the simulation diagram, as shown in Table 4 and in Figure 10.Table 4
CCSL specification and expression in TimeSquare.
CCSL specificationExpression in TimeSquareets∼asd∗ebnaExpressionc30 = Intersection(Clock1->asd, Clock2->ebna) and Relation r1[Alternates](AlternatesLeftClock -> ets, AlternatesRightClock -> c30)asd∨ebna ≼ eslExpressionc3 = Sup(Clock1->asd, Clock2->ebna) and Relation r2[Causes](LeftClock->c3, RightClock->esl)esl≺efa+efddelayedFor1onc1where clockc1=IdealClkdiscretizedBy4sExpressionc4 = Union(Clock1->efa,Clock2->efd) and cupp = DelayFor(DelayForClockToDelay->esl, DelayForClockForCounting->c4, DelayForDelay->d2)efd≡enoRelation r4[Coincides](Clock1->efd, Clock2->eno)efa∨asd≡efnaExpressioncsup = Sup(Clock1->efa, Clock2->asd) and Relation r5[Coincides](Clock1->csup, Clock2->efna)efa≺eso delayedFor1onc2where clockc2=IdealClkdiscretizedBy10sExpressioncupp1=DelayFor (DelayForClockToDelay->efa, DelayForClockForCounting->eso, DelayForDelay->d3)


## 5.1. Autonomous Overtaking Requirement Description for CADS

Although fully autonomous road vehicles (highway, urban traffic, and country roads) without human help/interruption remain futuristic, the automobile industries have been striving to meet these expectations. Academia and industry are committed to improve safety, reliability, and traffic efficiency and ease increasingly congested traffic situations. It is especially imperative for cooperative vehicles’ lane-changing and overtaking autonomously in the multilane highway. In this paper, we focus on autonomous driving behavior due to independent and self-sufficient decision-making function. These vehicles can communicate with surrounding relevant vehicles and the infrastructure to perceive traffic information. After understanding these environment perceptions, CADS generate negotiation maneuvers for autonomous lane-changing and overtaking behaviors. Each vehicle involving coordination observes its surrounding traffic and conforms to the generating decision-making to realize overtaking autonomously. In the following, requirements about lane-changing judgement, overtaking procedures, and message exchanging for autonomous overtaking are explained.We assume that there are three one-way lanes in this paper considering the situation shown in Figure9; the first lane is reserved_lane (lane 2 in Figure 9) occupied by ego_vehicle, the second lane is applying_lane (lane 3 in Figure 9) claimed to overtake by ego_vehicle, and the third lane is the right side of adjacent_lanes (lane 1 in Figure 9). According to the traffic code, we assume that ego_vehicle must claim the left-side adjacent_lane to complete the overtaking action driving on the right-hand side of the road. In the view of the ego_vehicle overtaking scenario, the following vehicles may be involved, and there may be exist three vehicles (ego_vehicle A, ego_front_vehicle B, and ego_behind_vehicle C) in the currently reserved_lane, two vehicles (applying_lane_behind_vehicle D and applying_lane_front_vehicle E) in the applying_lane, and one vehicle (adjacent_lane_vehicle F) in the adjacent_lane. When ego_vehicle on the currently occupied road has intention to overtake, the first is to turn on the left-turn signal to remind surrounding view vehicles of the lane-change intention. At this moment, there are three safety-critical matters to confirm; firstly, CADS should confirm whether vehicles in the applying_lane are within a safe distance; secondly, after the lane-change signal is observed by them, ego_behind_vehicle within the view cannot accelerate; and the third thing is to send an overtaking message to ego_front_vehicle in the same reserved_lane. After confirmation of overtaking in the first step, overtaking negotiation stage is followed. Ego_front_vehicle needs to reply agree or disagree within a certain time (response time, we assume 4 seconds) after receiving the overtaking message. If ego_vehicle cannot receive the reply message from ego_front_vehicle exceeding response time or receives the disagree message, it should not implement lane-changing overtaking behavior and need to keep the previous driving state. If safety distance constraints are not satisfied, overtaking cannot be implemented too. Only when two constraints (receiving agree message and safety distance) are satisfied at the same time, ego_vehicle can start to perform the first lane-changing action. Overtaking behavior can be decomposed into two-times lane-change actions. After the first lane-change mentioned above, ego_vehicle should speed up, and ego_front_vehicle replying agree message just now cannot accelerate. When ego_vehicle’s spatial position is greater than ego_front_vehicle and, meanwhile, they meet safety distance for the second lane-change action, ego_vehicle can implement the second lane-change. Time interval between two-times lane-changing must not exceed stipulated overtaking_time, such as 10 seconds. After ego_vehicle completes lane-change twice and overtakes ego_front_vehicle, CADS will automatically adjust speed and maintain a safety distance between them.Figure 9
View of the ego-vehicle overtaking.


## 5.2. CCSL for Autonomous Overtaking System (AOS) Specification

In order to present the multiclock autonomous overtaking system specification, we should show involved clocks during the overtaking process. For specifying convenience, each clock’s abbreviation is given. Next, we need to list various clocks: ego_turn_signal: ets, applying_lane_safedistance: asd, ego_behind_no_acceleration: ebna, ego_send_lanechange: esl, ego_front_agree: efa, ego_front_disagree: efd, ego_no_overtaking: eno, ego_front_no_acceleration: efna, and ego_send_overtaken: eso. The functional and timing properties of the AOS are specified as follows:AOS1: ego_turn_signal is always followed by applying_lane_safedistance and ego_behind_no_acceleration, so the corresponding CCSL constraint is thatets∼asd∗ebna.AOS2: applying_lane_safedistance and ego_behind_no_acceleration trigger (cause) event ego_send_lanechange. In other words, the slowest clockasd∨ebna is faster than both clocks asd and ebna, and the tick of clock asd∨ebna can trigger the occurrence of clock esl. The corresponding CCSL constraint is that asd∨ebna≼esl.AOS3: ego_front_agree or ego_front_disagree will occur after ego_send_lanechange within a response time of 4 s. The corresponding CCSL constraint is thatesl≺efa+efddelayedFor1onc1where clockc1=IdealClk discretized By4s.AOS4: when ego_vehicle receives the reply ego_front_disagree, it must trigger the event ego_no_overtaking simultaneously, and the CCSL constraint is thatefd≡eno.AOS5: clocks efa, asd, and efna satisfy the constraintsefa∨asd≡efna, which indicates that the slowest event between receiving ego_front_agree message and satisfying applying_lane_safedistance is faster than both of mentioned events, and ego_front_vehicle should trigger the event ego_front_no_acceleration simultaneously.AOS6: the event ego_send_overtaken will occur with 10 s after the event ego_front_agree. The corresponding CCSL constraint is that(18)efa≺eso delayed For1onc2where clockc2=IdealClk discretized By10s.


## 5.3. Model Validation through Model Simulation and Analysis for the AOS

After the multiclock AOS specification, we can perform model validation through clock constraint simulation intuitively. In the previous part, we present multiclock constraint AOS formal specifications by CCSL, and in this section, clock constraint checking results of model simulation are analyzed using the special tool TimeSquare, which yields a satisfying partial-order execution trace for multiclock constraints. The yielding traces are indicated as VCD format waveforms. When multiclock constraints are correct, TimeSquare will generate a valid simulation trace, but if CCSL specifications do not satisfy all clock constraints or have conflicts, the tool cannot execute and will result in a deadlock shown as the end of VCD waveform. One of the simulation traces is partially shown in Figure10. The blue and dashed arrows stand for the precedence clock relation, whereas red and vertical solid lines stand for the coincidence relation between two synchronous instants.Figure 10
One partial simulation trace for the autonomous overtaking system.Corresponding to safety-critical system properties, clock ego_turn_signal ets must happen alternatively with the intersection clock c30 of two clocks asd and ebna. The clock constraint simulation execution results are shown in Figure10, and CCSL specification and corresponding expressions in simulation tool TimeSquare are shown in Table 4. Clock constraint ets∼asd∗ebnais satisfied, and this safety-critical property is valid. We define the slowest clock c3 which is faster than clocks asd and ebna, and the tick of supremum clock c3 will cause the tick of clock esl; the result of this clock constraint is satisfied and shown as the clock waveform. Other functional properties are also satisfied and shown in the TimeSquare yielding trace; firstly, the clock efna will only tick if the slowest definition clock csup which is faster than clocks asd and efa is ticking synchronously. Secondly, another strictly synchronous clock constraint efd≡eno describes two events occurring in coincidence; event ego_front_disagree corresponding to clock efd means another event ego_vehicle cannot change the lane and implements overtaking behavior corresponding to clock eno; similarly, if ego_front_vehicle replies agreement, then it should not accelerate at the same time. As for timing nonfunctional properties, we combine coincidence and precedence mixed constraints. The clock specification cupp1=efa≺eso delayed For1onc2where clockc2=IdealClk discretized Byd3 constraints cupp1 to tick synchronously with d3th tick of clock eso, which follows a tick of clock efa, and cupp1 is a mixed constraint since eso and efa are asynchronous precedence clock relation in Table 1. It is similar to another DelayFor constraint cupp=esl≺efa+efddelayedFor1onc1where clockc1=IdealClk discretized Byd2, so the first time interval between sending and replying communicating message and the second time interval consumed during the process of overtaking are satisfied in the simulation diagram, as shown in Table 4 and in Figure 10.Table 4
CCSL specification and expression in TimeSquare.
CCSL specificationExpression in TimeSquareets∼asd∗ebnaExpressionc30 = Intersection(Clock1->asd, Clock2->ebna) and Relation r1[Alternates](AlternatesLeftClock -> ets, AlternatesRightClock -> c30)asd∨ebna ≼ eslExpressionc3 = Sup(Clock1->asd, Clock2->ebna) and Relation r2[Causes](LeftClock->c3, RightClock->esl)esl≺efa+efddelayedFor1onc1where clockc1=IdealClkdiscretizedBy4sExpressionc4 = Union(Clock1->efa,Clock2->efd) and cupp = DelayFor(DelayForClockToDelay->esl, DelayForClockForCounting->c4, DelayForDelay->d2)efd≡enoRelation r4[Coincides](Clock1->efd, Clock2->eno)efa∨asd≡efnaExpressioncsup = Sup(Clock1->efa, Clock2->asd) and Relation r5[Coincides](Clock1->csup, Clock2->efna)efa≺eso delayedFor1onc2where clockc2=IdealClkdiscretizedBy10sExpressioncupp1=DelayFor (DelayForClockToDelay->efa, DelayForClockForCounting->eso, DelayForDelay->d3)


## 6. Conclusion and Future Work

In recent years, the emergent multiclock constraint systems, e.g., autonomous driving systems, provide a great promise to our daily life. We are increasingly entrusting our lives to these software-dependent and safety-critical systems. Autonomous systems might seem fraught with danger on account of making individual or collaborative decisions by themselves. Developing multiclock autonomous systems becomes a challenging task because it is urgent and crucial that systems should anticipate the potential collisions, identify aberrant behaviors, and give early warning at the design time before systems’ deployment. In this paper, we propose a methodology to bridge the gap between design and analysis for cooperative and highly automated driving systems according to model-driven software development.Firstly, we have explored the modelling method in multiclock constraint context and presented relevant state-of-the-art specification and verification technologies in the cooperative autonomous driving domain. We firstly propose autonomous driving domain profile and CADS architecture for a motivation scenario and present the model-based simulation method, domain-specific modelling languages, and dedicated simulator TimeSquare. In order to perform model transformation, we give the syntax and state-based semantics of target multiclock constraint language. Secondly, in the model-driven safety-critical software design, model transformation is a frequently used technique. The operational semantics of both source and terminate languages, i.e., SysML state machine diagram and CCSL, has been formally specified in the form of labelled transition systems. We define strong bisimularity between SMD and CCSL. Behavioral equivalence and semantic preservation have been proven based on semantic mapping rules. Thirdly, through a cooperative autonomous overtaking case study, we use the proposed method to verify safety and reliability at the design phase, and simulation results indicate that the designed system can ensure safe autonomous overtaking driving behavior.Although this work adopts model-based development and model simulation helping to provide safety evidence, there also exist following limitations. The result of simulation is only one execution trace in terms of presumptions and is strongly dependent on the experience of system safety analysts. Model transformation is executed with a lot of human interactions. Furthermore, we plan to combine formal model checking, which can traverse all software execution traces, or theorem proving techniques to provide rigorous safeguard evidence. At the same time, we aim at developing an automatic transformation tool to realize automatic model transformation under semantic preservation mapping rules. In addition, we are considering to combine artificial intelligence technologies and model-driven software development together to design safe multiclock constraint autonomous systems.



---

*Source: 8830752-2020-12-07.xml*