Abstract Opacity serves as a critical security and confidentiality property, which concerns whether an intruder can unveil a system’s secret based on structural knowledge and observed behaviors. Opacity in timed systems presents greater complexity compared to untimed systems, and it has been established that opacity for timed automata is undecidable. However, the original proof cannot be applied to decide the opacity of one-clock timed automata directly. In this paper, we explore three types of opacity within timed automata: language-based timed opacity, initial-location timed opacity, and current-location timed opacity. We begin by formalizing these concepts and establishing transformation relations among them. Subsequently, we demonstrate the undecidability of the opacity problem for one-clock timed automata. Furthermore, we offer a constructive proof for the conjecture regarding the decidability of opacity for timed automata in discrete-time semantics. Additionally, we present a sufficient condition and a necessary condition for the decidability of opacity in specific subclasses of timed automata.

In model-driven design of embedded systems, how to generate code from high-level control models seamlessly and correctly is challenging. This is because hybrid systems are involved with continuous evolution, discrete jumps, and the complicated entanglement between them, while code only contains discrete actions. In this article, we investigate the code generation from Hybrid Communicating Sequential Processes (HCSP), a formal hybrid control model, to SystemC. We first introduce the notion of approximate bisimulation as a criterion to check the consistency between two different systems, especially between the original control model and the final generated code. We prove that it is decidable whether two HCSPs are approximately bisimilar in bounded time and unbounded time with some conditions, respectively. For both the cases, we present two sets of rules correspondingly for discretizing HCSPs and prove that the original HCSP model and the corresponding discretization are approximately bisimilar. Furthermore, based on the discretization, we define a transformation function to map a discretized HCSP model to SystemC code such that they are also approximately bisimilar. We finally implement a tool to automatically realize the translation from HCSP to SystemC code and illustrate our approach through some case studies.

Opacity is an important property on information flow to guarantee that a system under attack keeps its “secrets”, possibly subsets of traces (language-based opacity) or subsets of states (state-based opacity), opaque to the outside intruder with partial observability. In this paper, we investigate the opacity problems of real-time automata (RTA), which is a popular model for real-time systems. In order to prove that the language-opacity problem of RTA is decidable, we introduce the notion of trace-equivalence and then translate RTA into finite-state automata (FA) with timed alphabets. Besides, we also introduce the notions of partitioned timed alphabet and language to guarantee trace equivalence is preserved by complementation and product operations over FA with timed alphabets. Thus, our decision procedure can be sketched as follows: first, translate the RTA to model a system under attack and the RTA to specify the secret behavior of the system into FA, respectively; then, compute another FA, which accepts all traces accepted by the first FA, but not by the second one; afterwards, project these FA onto the given observable set; finally, unify the alphabets of these FA such that for any two timed actions with the same event, their time parts do not have any overlap. Thus, whether the original system is language-opaque with respect to the secret RTA and the observable set is reduced to the inclusion problem of regular languages. Similarly, we can show decidability of initial-opacity of RTA.