Article Preview
TopIntroduction
Cyber-physical systems (CPSs) refer to a new generation of systems with integrated computational and physical capabilities that can interact with humans through many new modalities (Gupta, Kumar, Hansel, & Saini, 2013). The ability to interact with, and expand the capabilities of, the physical world through computation, communication, and control is a key enabler for future technology developments. Opportunities and research challenges include the design and development of next-generation airplanes and space vehicles, hybrid gas-electric vehicles, fully autonomous urban driving, and prostheses that allow brain signals to control physical objects. Control is time sensitive. So, the timing behaviors modeling and verification for CPSs is essential.
What is more, the time in CPSs is important to functional correctness. For example, in general-purpose software, the time it takes to perform a task is an issue of performance, not correctness. It is not incorrect to take longer to perform a task. It is merely less convenient and therefore less valuable. In CPS, the time it takes to perform a task may be critical to correct functioning of the system. Also, the data’s validity is strictly restricted by time. There are complex dependency relations on variables (data) and time. In CPSs, the timing behaviors have the following three characteristics:
- ●
Periodicity: CPSs are widely used to provide control over the physical process through control loops. They monitor the physical process through sensors and interact with the physical process through actuators. Due to the existence of the control loop, periodicity is inevitably generated.
- ●
Multiform time: The CPSs software is of logical time. CPSs face a variety of environments, including various devices, existing systems, and humans. Such an environment is of physical time, but it may be diverse in time description. For example, distance meters or angles can be used to describe time. Both physical time and logical time are covered. This is called multiform time.
- ●
Time synchronization: In the physical world, processes are rarely sequential. Physical processes are compositions of many parallel sub-processes. Measuring and controlling the dynamics of these processes by orchestrating actions that influence the processes are the main tasks of embedded systems. Consequently, synchronization between concurrency is intrinsic in CPSs.
Existing CPS timing behaviors modeling researches can be mainly divided into semi-formal modeling and formal modeling. Semi-formal modeling mainly refers to Unified Modeling Language (UML) (OMG, 2007) and its extended language modeling, including sequence diagram, timing diagram, clock constraint language CCSL and so on. For example, Choi et al. used a state machine with a MARTE annotation, a timing diagram, and a sequence diagram to describe the timing behaviors (Choi, Jee, & Bae, 2016). Semi-formal modeling is relatively easy to describe for timing behaviors, but the description is not accurate enough. Formal modeling mainly includes Timed Automata (Alur & Dill, 1994; Lynch & Vaandrager, 1996), Timed Communication Sequence Process (Timed CSP) (Schneider, 1995), Timed Petri Nets (Ramchandani, 1974), etc. For example, Sun et al. support the modeling and verification of real-time systems using the Stateful Timed CSP (Sun et al., 2013). Formal modeling is accurate, but it is difficult to grasp for people with high learning costs and poor mathematical foundations.