Abstract
Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. However, succintness and visual structure of a timing diagram are not adequately captured by their formulae [6]. Interval temporal logic QDDC is a highly succint and visual notation for specifying patterns of behaviours [15]. In this paper, we propose a practically useful notation called SeCeNL which enhances the quantifier and negation free fragment of QDDC with features of nominals and limited liveness. We show that for SeCeNL, the satisfiability and model checking problems have elementary complexity as compared to the non-elementary complexity for the full logic QDDC. Next we show that timing diagrams can be naturally, compositionally and succintly formalized in SeCeNL as compared with PSL-Sugar and MTL. We give a linear time translation from timing diagrams to SeCeNL. As our second main result, we propose a linear time translation of SeCeNL into QDDC. This allows QDDC tools such as DCVALID [15, 16] and DCSynth [17] to be used for checking consistency of timing diagram requirements as well as for automatic synthesis of property monitors and controllers. We give an example of a minepump controller to illustrate our tools.
Notes
- 1.
Hence the logic is called QDDC which abbreviates Quantified Discrete Duration Calculus.
- 2.
The illustration was made with WaveDrom and due to its limitation on naming nominals we were forced to rename the nominals u and v in Q as a and b respectively.
References
Allen, J.F.: Maintaining knowledge about temporal intervals. Comm. ACM 26(11), 832–843 (1983)
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)
Amla, N., Emerson, E.A., Kurshan, R.P., Namjoshi, K.S.: Model checking synchronous timing diagrams. In: FMCAD 2000, pp. 283–298 (2000)
Babu, A., Pandya, P.K.: Chop expressions and discrete duration calculus. In: Modern Applications of Automata Theory, pp. 229–256 (2012)
Chapyzhenka, A., Probell, J.: Wavedrom: rendering beautiful waveforms from plain text. Synopsys User Group (2016). http://wavedrom.com/images/SNUG2016_WaveDrom.pdf
Chockler, H., Fisler, K.: Temporal modalities for concisely capturing timing diagrams. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 176–190. Springer, Heidelberg (2005). doi:10.1007/11560548_15
Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Form. Methods Syst. Des. 19(1), 45–80 (2001)
Eisner, C., Fisman, D.: Temporal logic made practical. In: Handbook of Model Checking. Springer (2016, expected). http://www.cis.upenn.edu/~fisman/documents/EF_HBMC14.pdf
Fisler, K.: Timing diagrams: formalization and algorithmic verification. J. Logic Lang. Inform. 8(3), 323–361 (1999)
Fisler, K.: Two-dimensional regular expressions for compositional bus protocols. In: FMCAD 2007, pp. 154–157 (2007)
Franceschet, M., de Rijke, M., Schlingloff, B.: Hybrid logics on linear structures: expressivity and complexity. In: TIME-ICTL 2003, pp. 166–173 (2003)
Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theor. Comp. Sci. 331(2–3), 397–428 (2005)
Matteplackel, R.M., Pandya, P.K., Wakankar, A.: Formalizing timing diagram requirements in discrete duration calulus. CoRR abs/1705.04510 (2017)
Pandya, P.K., Ramakrishna, Y.S., Shyamasundar, R.K.: A compositional semantics of esterel in duration calculus. In: AMAST 1995 (1995)
Pandya, P.K.: Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. In: RTTOOLS 2001, Affiliated with CONCUR (2001)
Pandya, P.K.: Model checking CTL*[DC]. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 559–573. Springer, Heidelberg (2001). doi:10.1007/3-540-45319-9_38
Wakankar, A., Pandya, P.K., Matteplackel, R.M.: DCSynth: guided reactive synthesis with soft requirements and performance measurement. CoRR (2017)
WaveDrom: Wavedrom user manual (2016). http://wavedrom.com/tutorial.html
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Matteplackel, R.M., Pandya, P.K., Wakankar, A. (2017). Formalizing Timing Diagram Requirements in Discrete Duration Calculus. In: Cimatti, A., Sirjani, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10469. Springer, Cham. https://doi.org/10.1007/978-3-319-66197-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-66197-1_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66196-4
Online ISBN: 978-3-319-66197-1
eBook Packages: Computer ScienceComputer Science (R0)