Abstract
This paper presents an assume-guarantee specification theory (aka interface theory from [11]) for modular synthesis and verification of real-time processes with critical timing constraints. Four operations, i.e. conjunction, disjunction, parallel and quotient, are defined over specifications, drawing inspirations from classic specification theories like refinement calculus [4, 19]. We show that a congruence (or pre-congruence) characterised by a trace-based semantics [14] captures exactly the notion of substitutivity (or refinement) between specifications.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Note that the existence of incompatibility errors does not mean that the composed system is un-usable; an environment can still usefully exploit the system by only utilising the part of the system that is free of the incompatibility errors, as has been well explained in [11].
- 2.
It were Carroll Morgan and Joseph M. Morris who first added miracle to refinement calculus.
- 3.
Our timed framework originally appeared in [9]. However, the version presented here contains important technical extension as well as presentational improvements.
- 4.
Invariants and guards on output actions are constraints on the system (aka guarantees) whereas co-invariants and guards on input actions are constraints on the environment (aka assumptions).
- 5.
\(\mathcal {P}\) is time-additive providing \(p \xrightarrow {d_1+d_2} s'\) iff \(p \xrightarrow {d_1} s\) and \(s \xrightarrow {d_2} s'\) for some \(s \in S\).
- 6.
Note that invariant and co-invariant are downward-closed. Thus, the only way to violate them is to exceed their upper bounds.
- 7.
One further case missing above is that, for an action transition, there is possibility that its guard is respected but the invariant/co-invariant of its destination (say l) is violated. In such situation, a state (l, t) is treated (1) as \(\top \) if t violates the invariant in location l and (2) as \(\bot \) if t violates the co-invariant in l while the invariant holds.
- 8.
For \(i \in \{0,1\}\) and \(p_i=(l_i, t_i)\), \(p_0 \times p_1 = ((l_0,l_1),t_0 \uplus t_1)\) (t0 and \(t_1\) are clock-disjoint).
- 9.
Containment of \(\rightarrow _0 \cup \rightarrow _1\) is not required for parallel composition, but is necessary for conjunction and disjunction.
- 10.
The technique was inspired by a discussion with Roscoe on angelic choice in CSP.
- 11.
Note that the above definition exploits the fact that the addition or removal of false-guarded transitions to AT will not change the semantics of the automata.
- 12.
The modified determinisation procedure first appeared in the Definition 4.2 of [26], which is for the untimed case.
- 13.
We say an acyclic TIOTS is a tree if (1) there does not exist a pair of transitions in the form of \(p \xrightarrow {a} p''\) and \(p' \xrightarrow {d} p''\), (2) \(p \xrightarrow {a} p'' \wedge p' \xrightarrow {b} p''\) implies \(p=p'\) and \(a=b\) and (3) \(p \xrightarrow {d} p'' \wedge p' \xrightarrow {d} p''\) implies \(p=p'\).
- 14.
For the former, \(\mathcal {G}_s\) generates exactly a time interval (0, d] of delays from p, after which \(\mathcal {G}_s\) arrives at another plain state with a enabled. For the latter, an infinite time interval \((0,\infty )\) of delays are enabled at p. The delays either all lead to plain states or \((0,\infty )\) can be further partitioned into two intervals s.t. the delays in the first interval lead to plain states while those of the second lead to \(\top \) or \(\bot \).
- 15.
We choose not to call it a winning strategy as it serves additional purpose for our paper.
- 16.
Given a \(\top /\bot \) complete interface, we say a plain state p is an auto-\(\top \) iff \(p \xrightarrow {a} \top \) for some \(a \in I\); a plain state p is a semi-\(\top \) iff (1) all output transitions in p or any of its time-passing successors lead to the \(\top \) state, and (2) there exists \(d \in \mathbb {R}^{>0}\) s.t. \(p \xrightarrow {d} \top \).
- 17.
We omit the two operators in this paper due to space limitation.
- 18.
That is, they can distinguish the \(\bot \) state from the \(\bot \)-winning states by stopping time immediately.
- 19.
It is easy to verify that realisable specifications are closed under \(\parallel \) defined in Sect. 3 since \(\parallel \) preserves auto-\(\top \) and semi-\(\top \) freedom.
- 20.
With the extension, blocked synchronisation, i.e. an action being enabled on one process but not so on the other, becomes possible.
- 21.
- 22.
- 23.
The mirror-based definition of quotient (for the untimed case) was first presented by Verhoeff as his Factorisation Theorem [24].
- 24.
Composition of untimed specifications will not generated new unrealisable behaviours.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
Armstrong, P.J., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking timed CSP. In: A Festschrift on the Occasion of H. Barringer’s 60th Birthday (2014)
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symposium on System Structure and Control, Elsevier (1998)
Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)
Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.: Contracts for systems design. Technical report RR-8147, S4 team, INRIA, November 2012
Bertrand, N., Stainer, A., Jéron, T., Krichen, M.: A game approach to determinize timed automata. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 245–259. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19805-2_17
Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). doi:10.1007/11539452_9
Chilton, C., Jonsson, B., Kwiatkowska, M.: Compositional assume-guarantee reasoning for input/output component theories. Sci. Comput. Program. 91, 115–137 (2014). Part A
Chilton, C., Kwiatkowska, M., Wang, X.: Revisiting timed specification theories: a linear-time perspective. In: FORMATS 2012 (2012)
David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: HSCC 2010 (2010)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE 2001 (2001)
de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: EMSOFT 2002, vol. 2491, pp. 108–122 (2002)
de Alfaro, L., Stoelinga, M.: Interfaces: a game-theoretic framework for reasoning about component-based systems. Electron. Notes Theoret. Comput. Sci. 97, 3–23 (2004)
Dill, D.L.: Trace theory for automatic hierarchical verification of speed-independent circuits. In: ACM Distinguished Dissertations. MIT Press (1989)
Ebergen, J.C.: A technique to design delay-insensitive VLSI circuits. Technical report CS-R8622, Centrum voor Wiskunde en Informatica, June 1986
He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986). doi:10.1007/3-540-16442-1_14
Hoare, C.A.R., He, J., Sanders, J.W.: Prespecification in data refinement. Inf. Process. Lett. 25(2), 71–76 (1987)
Meyer, B.: Design by contract. In: Advances in Object-Oriented Software Engineering. Prentice Hall (1991)
Morgan, C.C.: Programming from Specifications. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, UK (1994)
Negulescu, R.: Process spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 199–213. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_16
Reed, G.M., Roscoe, A.W., Schneider, S.A.: CSP and Timewise Refinement, pp. 258–280. Springer, London (1991)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, UK (1998)
van de Snepscheut, J.L.A.: Trace Theory and VLSJ Design. LNCS, vol. 200. Springer, Heidelberg (1985)
Verhoeff, T.: A Theory of Delay-Insensitive Systems. Ph.D. thesis, Dept. of Math. and C.S., Eindhoven University of Technology, May 1994
Wang, X.: Maximal confluent processes. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 188–207. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31131-4_11
Wang, X., Kwiatkowska, M.Z.: On process-algebraic verification of asynchronous circuits. Fundam. Inform. 80(1–3), 283–310 (2007)
Acknowledgments
We benefit from discussions with Prof. David Dill and Prof. Jeff Sanders on timed extension of trace theory and refinement calculus.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Chilton, C., Kwiatkowska, M., Moller, F., Wang, X. (2017). A Specification Theory of Real-Time Processes. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds) Concurrency, Security, and Puzzles. Lecture Notes in Computer Science(), vol 10160. Springer, Cham. https://doi.org/10.1007/978-3-319-51046-0_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-51046-0_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-51045-3
Online ISBN: 978-3-319-51046-0
eBook Packages: Computer ScienceComputer Science (R0)