The polychronous or multi-clock paradigm is adequate to model large distributed systems where achieving a full timed synchronization is not only very costly but also often not necessary. It concerns systems made of a set of components with loose synchronization constraints. We study an approach where those components are orchestrated using logical clocks , made popular by L. Lamport and synchronous languages. The temporal and causal specification of those systems is built by defining a set of clock relations that would constrain the instant when clocks can tick or must not tick, thus defining families of valid schedules . In this article, we propose a specification language, called \(\mathit {LTL}_c/\mathit {CCSL}\) , for specifying temporal properties of multi-clock systems. While traditional temporal logics (LTL, MTL, CTL*), whether linear or branching, rely on a global step, our language, \(\mathit {LTL}_c/\mathit {CCSL}\) , builds a partial order on logical clocks, thus allowing both a hierarchical approach based on refinement of clock hierarchies and compositionality, as what happens in one clock domain may remain largely independent of what may happen in other domains. This good property helps preserve the properties without requiring to perform the proofs again. An \(\mathit {LTL}_c/\mathit {CCSL}\) specification consists of a clock temporal logic \(\mathit {LTL}_c\) , accompanied by a clock calculus called CCSL for specifying clock relations. We build the syntax and semantics of \(\mathit {LTL}_c\) and link its semantics with CCSL. After that, we mainly focus on the verification aspect of \(\mathit {LTL}_c/\mathit {CCSL}\) specifications using a model checking technique. We show how \(\mathit {LTL}_c/\mathit {CCSL}\) can be used for specifying multi-clock systems with an example.

Cyber-physical systems (CPSs) have emerged as a potential enabling technology to handle the challenges in social and economic sustainable development. Since it was proposed in 2006, intensive research has been conducted, showing that the construction of a CPS is a hard and complex engineering process due to the nature of integrating a large number of heterogeneous subsystems. Among other approaches to dealing with the complex design issues, model-driven design of CPSs has shown its advantages. In this review paper, we present a survey of research on model-driven development of CPSs. We are concerned mainly with the widely used methods, techniques, and tools, and discuss how these are applied to CPSs. We also present comparative analyses on the surveyed techniques and tools from various perspectives, including their modeling languages, functionalities, and the challenges which they address in CPS design. With our understanding of the surveyed methods, we believe that model-driven approaches are an inevitable choice in building CPSs and further research effort is needed in the development of model-driven theories, techniques, and tools. We also argue that a unified modeling platform is needed. Such a platform would benefit research in the academic community and practical development in industry, and improve the collaboration between these two communities.

The Clock Constraint Specification Language (CCSL) is a clock-based formalism for formal specification and analysis of real-time embedded systems. Previous approaches for the schedulability analysis of CCSL specifications are mainly based on model checking or SMT-checking. In this paper we propose a logical approach mainly based on theorem proving. We build a dynamic logic called 'clock-based dynamic logic' (cDL) to capture the CCSL specifications and build a proof calculus to analyze the schedule problem of the specifications. Comparing with previous approaches, our method benefits from the dynamic logic that provides a natural way of capturing the dynamic behaviour of CCSL and a divide-and-conquer way for 'decomposing' a complex formula into simple ones for an SMT-checking procedure. Based on cDL, we outline a method for the schedulability analysis of CCSL. We illustrate our theory through one example.

Intelligent Transportation Systems (ITS) are a class of quickly evolving modern safety-critical embedded systems. Dealing with their growing complexity demands a high-level formal modeling language along with adequate verification techniques. STeC has recently been introduced as a process algebra that deals natively with both spatial and temporal properties. Even though STeC has the right expressive power, it does not provide a direct tooled support for verification. We propose to encode STeC specifications as Timed Automata to provide such a support and we illustrate our transformation strategy on a simple example.