Structural transformations for data-enriched real-time systems
Pages 727 - 750
Abstract
We investigate design-level structural transformations that aim at easier subsequent verification of real-time systems with shared data variables, modelled as networks of extended timed automata (ETA). Our contributions to this end are the following: (1) we first equip ETA with an operator for layered composition, intermediate between parallel and sequential composition. Under certain non-interference and/or precedence conditions imposed on the structure of the ETA networks, the communication closed layer (CCL) laws and associated partial-order (po-) and (layered) reachability equivalences are shown to hold. (2) Next, we investigate (under certain cycle conditions on the ETA) the (reachability preserving) transformations of separation and flattening aimed at reducing the number of cycles of the ETA. (3) We then show that our separation and flattening in (2) may be applied together with the CCL laws in (1), in order to restructure ETA networks such that the verification of layered reachability properties is rendered easier. This interplay of the three structural transformations (separation, flattening, and layering) is demonstrated on an enhanced version of Fischer’s real-time mutual exclusion protocol for access to multiple critical sections.
References
References
[1]
Alur R. and Dill D. A theory of timed automata TCS 1994 126 2 183-235
[2]
Behrmann G, David A, Larsen KG (2004) A tutorial on Uppaal. In: Formal methods for the design of real-time systems, vol 3185 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 200–236
[3]
Bengtsson J, Jonsson B, Lilius J, Yi W (1998) Partial order reductions for timed systems. In: Sangiorgi D, de Simone R (eds) CONCUR, vol 1466 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 485–500
[4]
Bochmann GV Distributed synchronization and regularity Comput Netw 1979 3 36-43
[5]
Bochmann GV Delay-independent design for distributed systems IEEE Trans Softw Eng 1988 14 8 1229-1237
[6]
Bouyer P, Petit A (1999) Decomposition and composition of timed automata. In: Wiedermann J, van Emde Boas P, Nielsen M (eds) ICALP, vol 1644 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 210–219
[7]
Bornot S and Sifakis J An algebraic framework for urgency Inf Comput 2000 163 172-202
[8]
Comon H, Jurski Y (1999) Timed automata and the theory of real numbers. In: Baeten JCM, Mauw S (eds) CONCUR, vol 1664 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 242–257
[9]
Chandy KM and Misra J Parallel program design—a foundation 1988 USA Addison Wesley
[10]
Cohen E (2000) Separation and reduction. In: Backhouse RC, Oliveira JN (eds) Mathematics of program construction, vol 1837 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 45–59
[11]
Chaouch-Saad M, Charron-Bost B, Merz S (2009) A reduction theorem for the verification of round-based distributed algorithms. In: Bournez O, Potapov I (eds) Reachability problems, vol 5797 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 93–106
[12]
Dong JS, Hao P, Qin S, Sun J, and Yi W Timed automata patterns IEEE Trans Softw Eng 2008 34 6 844-859
[13]
Dräger K, Kupriyanov A, Finkbeiner B, Wehrheim H (2010) Slab: a certifying model checker for infinite-state concurrent systems. In: Esparza J, Majumdar R (eds) TACAS, vol 6015 of LNCS, pp 271–274
[14]
Elrad T and Francez N Decomposition of distributed programs into communication-closed layers Sci Comput Program 1982 2 155-173
[15]
Haakansson J, Pettersson P (2007) Partial order reduction for verification of real-time components. In: Raskin J.-F, Thiagarajan PS (eds) FORMATS, vol 4763 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 211–226
[16]
Havelund K, Skou A, Larsen KG, Lund K (1997) Formal modeling and analysis of an audio/video protocol: an industrial case study using uppaal. In: RTSS. IEEE Computer Society, pp 2–13
[17]
Janssen W (1994) Layered design of parallel systems. PhD thesis, University of Twente
[18]
Janssen W, Poel M, Xu Q, Zwiers J (1994) Layering of real-time distributed processes. In: Langmaack H, de Roever WP, Vytopil J (eds) FTRTFT, vol 863 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 393–417
[19]
Kushilevitz E, Rabin MO (1992) Randomized mutual exclusion algorithms revisited. In: PODC. ACM Press, pp 275–283
[20]
Lugiez D, Niebert P, and Zennou S A partial order semantics approach to the clock explosion problem of timed automata Theor Comput Sci 2005 345 27-59
[21]
Larsen KG, Steffen B, and Weise C (1996) Fischer’s protocol revisited: a simple proof using modal constraints. In: Alur R, Henzinger TA, Sontag ED (eds) Hybrid systems, vol 1066 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 604–615
[22]
Milner R Communication and concurrency 1986 USA Prentice Hall
[23]
Minea M (1999) Partial order reduction for model checking of timed automata. In: Baeten JCM, Mauw S (eds) CONCUR, vol 1664 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 431–436
[24]
Muniz M, Westphal B, Podelski A (2012) Timed automata with disjoint activity. In: Jurdzinski M, Nickovic D (eds) FORMATS, vol 7595 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 188–203
[25]
Olderog E.-R and Dierks H Real-time systems—formal specification and automatic verification 2008 Cambridge Cambridge University Press
[26]
Olderog E.-R, Swaminathan M (2010) Layered composition for timed automata. In: Chatterjee K, Henzinger TA (eds) FORMATS, vol 6246 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 228–242
[27]
Olderog E.-R, Swaminathan M (2013) Structural transformations for data-enriched real-time systems. In: Johnsen EB, Petre L (eds) iFM, vol 7940 of LNCS. Springer-Verlag, Berlin Heidelberg, pp 378–393
[28]
Peter H.-J, Mattmüller R (2009) Component-based abstraction refinement for timed controller synthesis. In: RTSS. IEEE Computer Society, pp 364–374
[29]
Stomp FA and de Roever W.-P A principle for sequential reasoning about distributed algorithms Form Asp Comput 1994 6 6 716-737
[30]
Sharma A, Katoen J.-P (2014) Layered reduction for abstract probabilistic automata. In: ACSD. IEEE Computer Society (to appear)
[31]
Sharma A, Katoen J.-P (2014) Layered reduction for modal specification theories. In: Fiadeiro JL, Liu Z, Xue J (eds) FACS, vol 8348 of LNCS. Springer-Verlag, Berlin Heidelberg
[32]
Swaminathan M, Katoen J.-P, and Olderog E.-R Layered reasoning for randomized distributed algorithms Form Asp Comput 2012 24 477-496
Index Terms
- Structural transformations for data-enriched real-time systems
Index terms have been assigned to the content through auto-classification.
Recommendations
Data-only flattening for nested data parallelism
PPoPP '13: Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programmingData parallelism has proven to be an effective technique for high-level programming of a certain class of parallel applications, but it is not well suited to irregular parallel computations. Blelloch and others proposed nested data parallelism (NDP) as ...
Data-only flattening for nested data parallelism
PPoPP '13Data parallelism has proven to be an effective technique for high-level programming of a certain class of parallel applications, but it is not well suited to irregular parallel computations. Blelloch and others proposed nested data parallelism (NDP) as ...
Enabling unimodular transformations
Supercomputing '94: Proceedings of the 1994 ACM/IEEE conference on SupercomputingThe development of a unimodular transformation theory and associated algorithms has renewed interest in Fortran do loops that are not perfectly (or tightly) nested. In this paper we summarize a number of techniques that convert imperfectly nested loops ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© British Computer Society 2014.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 July 2015
Accepted: 27 May 2014
Revision received: 30 April 2014
Received: 30 November 2013
Published in FAC Volume 27, Issue 4
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 47Total Downloads
- Downloads (Last 12 months)37
- Downloads (Last 6 weeks)8
Reflects downloads up to 12 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in