This paper presents a novel approach to including non-instantaneous discrete control transitions in the linear hybrid automaton approach to simulation and verification of hybrid control systems. In this paper we study the control of a continuously evolving analog plant using a controller programmed in a synchronous programming language. We provide extensions to the synchronous subset of the SystemJ programming language for modeling, implementation, and verification of such hybrid systems. We provide a sound rewrite semantics that approximate the evolution of the continuous variables in the discrete domain inspired from the classical supervisory control theory. The resultant discrete time model can be verified using classical model-checking tools. Finally, we show that systems designed using our approach have a higher fidelity than the ones designed using the hybrid automaton approach.
Finally, the work closest to the one described in this article is done by: (1) @cite_2 , where they extend the Esterel language to model timed automata @cite_1 , i.e., ODEs with rate of change always equal to 1. In this proposal we are able to model the more general hybrid rather than its subset timed automaton and (2) @cite_12 , which is a seminal work in extending synchronous imperative languages to model hybrid automaton. This work is extended further and completed by giving a formal treatment by @cite_13 . The work described herein differs significantly from both; @cite_13 and @cite_12 in that they do not approximate the continuous behavior of the plant, instead all discrete transitions are carried out and then a so called continuous phase is launched, which models the continuous evolution of the plant until the invariant condition holds, just like in hybrid automaton. Since these approaches derive their semantics from hybrid automaton, they inherit the same problem described in , i.e., non-zero mode-switch transitions cannot be captured in the semantics.
@cite_13 @cite_1 @cite_12 @cite_2
2149007581 2101508170 2007068025 2116912109
In this paper, we present an extension of the synchronous language Quartz by new kinds of variables, actions and statements for modeling the interaction of synchronous systems with their continuous environment. We present an operational semantics of the obtained hybrid modeling language and moreover show how compilation algorithms that have been originally developed for synchronous languages can be extended to these hybrid programs. Thus, we can automatically translate the hybrid programs to compact symbolic representations of hybrid transition systems that can be immediately used for simulation and formal verification. Alur, R. and D.L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183-235. We propose timed (j&e) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words-infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Biichi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable (II i-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems. Abstract A hallmark of the Esterel language is the combination of perfect synchrony with total orthogonality and powerful constructs for preemption, suspension and trap handling. It is desirable to make this kind of expressiveness available for the description of hybrid systems, that is, systems whose evolution is understood in terms of segment-wise continuous functions over the real time axis. Our approach consists of modifying Esterel concepts, most notably by replacing the discrete time frame by a continuously advancing one. We are then able to state a semantics made up of transitions with closed execution intervals of non-zero length. By an instant we understand an execution interval within this framework. Hybrid signals may change their value during such an instant, non-hybrid ones, that is, classical signals immediately settle to a specific state and keep it the whole time. Time consumption still has to be specified explicitly, namely in that instants reflect jumps among control flow locations defined by pause statements; all other statements take no time in the sense that arbitrarily many of them may be sequentially executed regardless of the instant's duration. A transfer of perfect synchrony from the discrete to the continuous is in this way accomplished. We also consider an example, which is from the automotive domain, traces, bisimilarity and compositionality. The goal of TAXYS is to provide a framework for developing real-time embedded code and verifying its correct behavior with respect to quantitative timing requirements. To achieve so, TAXYS connects France Telecom's ESTEREL compiler SAXO-RT with VERIMAG's model-checker KRONOS. TAXYS has been successfully applied to real industrial telecommunication systems, such as a GSM radio link from Alcatel and a phone prototype from France Telecom.