Translating synchronous guarded actions to interleaved guarded actions
Pages 167 - 176
Abstract
In general, guarded actions are well suited to describe systems with different models of computations (MoCs). Different MoCs are thereby obtained by different ways to select actions for execution: In particular, in synchronous models, one executes all enabled actions, in interleaved models, one executes one of the enabled actions, and in asynchronous models, some non-empty subset of the enabled actions is executed. It seems to be impossible to use tools for one of these MoCs for guarded actions that are based on another MoC. In particular, it is unfortunate for the synchronous models that many rewrite-based verification tools and theorem provers are based on interleaved MoCs. In this paper, we therefore develop a translation from synchronous guarded actions (SGAs) to interleaved guarded actions (IGAs). This allows us to use many established tools for formal verification also for systems represented by SGAs. To achieve this, we have to solve four major problems: first, the causal execution order of the synchronous guarded actions must be encoded in the IGAs. Second, the different behaviors of immediate and delayed assignments of our SGAs must be preserved. Third, it must be guaranteed that all IGAs of one macro step are executed before the IGAs of the next macro step are started. Finally, temporal logic specifications stated for the SGAs have to be adequately adapted for IGAs. Our results are finally used to verify SGAs obtained by compilation of synchronous programs by means of the symbolic analysis laboratory (SAL) of SRI.
References
[1]
D. Harel and A. Pnueli, "On the development of reactive systems," in Logic and Models of Concurrent Systems, K. Apt, Ed. Springer, 1985, pp. 477-498.
[2]
N. Halbwachs, Synchronous programming of reactive systems. Kluwer, 1993.
[3]
A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone, "The synchronous languages twelve years later," Proceedings of the IEEE, vol. 91, no. 1, pp. 64-83, 2003.
[4]
G. Berry and G. Gonthier, "The Esterel synchronous programming language: Design, semantics, implementation," Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[5]
K. Schneider, "The synchronous programming language Quartz," Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, Internal Report 375, December 2009.
[6]
K. Schneider, "Embedding imperative synchronous languages in interactive theorem provers," in Application of Concurrency to System Design (ACSD). Newcastle Upon Tyne, England, UK: IEEE Computer Society, 2001, pp. 143-154.
[7]
L. de Moura, S. Owre, H. Rueß, J. Rushby, N. Shankar, M. Sorea, and A. Tiwari, "SAL 2," in Computer Aided Verification (CAV), ser. LNCS, R. Alur and D. Peled, Eds., vol. 3114. Boston, Massachusetts, USA: Springer, 2004, pp. 496-500.
[8]
J.-R. Abrial, Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
[9]
Arvind, "Bluespec: A language for hardware design, simulation, synthesis and verification invited talk," in Formal Methods and Models for Codesign (MEMOCODE). Mont Saint-Michel, France: IEEE Computer Society, 2003, pp. 249-254.
[10]
G. Singh and S. Shukla, "Algorithms for low power hardware synthesis from concurrent action oriented specifications CAOS," International Journal of Embedded Systems (IJES), vol. 3, no. 1/2, pp. 83-92, 2007.
[11]
D. Dill, "The Murphi verification system," in Computer Aided Verification (CAV), ser. LNCS, R. Alur and T. Henzinger, Eds., vol. 1102. New Brunswick, New Jersey, USA: Springer, 1996, pp. 390-393.
[12]
K. Chandy and J. Misra, Parallel Program Design. Austin, Texas, USA: Addison-Wesley, May 1989.
[13]
E. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs," Communications of the ACM (CACM), vol. 18, no. 8, pp. 453-457, 1975.
[14]
N. Halbwachs, "A synchronous language at work: the story of Lustre," in Formal Methods and Models for Codesign (MEMOCODE). Verona, Italy: IEEE Computer Society, 2005, pp. 3-11.
[15]
P. Le Guernic, T. Gauthier, M. Le Borgne, and C. Le Maire, "Programming real-time applications with SIGNAL," Proceedings of the IEEE, vol. 79, no. 9, pp. 1321-1336, 1991.
[16]
C. André, "SyncCharts: A visual representation of reactive behaviors," University of Nice, Sophia Antipolis, France, Research Report tr95-52, 1995.
[17]
M. Gesell and K. Schneider, "Modular verification of synchronous programs," in Application of Concurrency to System Design (ACSD), J. Carmona Mihai, T. Lazarescu, and M. Pietkiewicz-Koutny, Eds. Barcelona, Spain: IEEE Computer Society, 2013, pp. 77-86.
[18]
J. Brandt and K. Schneider, "Separate compilation for synchronous programs," in Software and Compilers for Embedded Systems (SCOPES), ser. ACM International Conference Proceeding Series, H. Falk, Ed., vol. 320. Nice, France: ACM, 2009, pp. 1-10.
[19]
K. Schneider, J. Brandt, T. Schüle, and T. Türk, "Improving constructiveness in code generators," in Synchronous Languages, Applications, and Programming (SLAP), Edinburgh, Scotland, UK, 2005, pp. 1-19.
[20]
K. Schneider, J. Brandt, and T. Schüle, "Causality analysis of synchronous programs with delayed actions," in Compilers, Architecture, and Synthesis for Embedded Systems (CASES). Washington, District of Columbia, USA: ACM, 2004, pp. 179-189.
[21]
J. Brandt and K. Schneider, "Formal reasoning about causality analysis," in Theorem Proving in Higher Order Logics (TPHOL), ser. LNCS, O. A. Mohamed, C. Muñoz, and S. Tahar, Eds., vol. 5170. Montréal, Québec, Canada: Springer, 2008, pp. 118-133.
[22]
G. Berry, "The Esterel v5 language primer," July 2000.
[23]
G. Berry, "The constructive semantics of pure Esterel," July 1999.
[24]
C. Hoare, "Communicating sequential processes," Communications of the ACM (CACM), vol. 21, no. 8, pp. 666-677, 1978.
[25]
J. Brandt, M. Gemünde, and K. Schneider, "From synchronous guarded actions to SystemC," in Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), M. Dietrich, Ed. Dresden, Germany: Fraunhofer Verlag, 2010, pp. 187-196.
[26]
D. Baudisch, J. Brandt, and K. Schneider, "Translating synchronous systems to data-flow process networks," in Parallel and Distributed Computing, Applications and Technologies (PDCAT), S.-S. Yeo, B. Vaidya, and G. Papadopoulos, Eds. Gwangju, Korea: IEEE Computer Society, 2011, pp. 354-361.
[27]
K. Schneider and J. Brandt, "Performing causality analysis by bounded model checking," in Application of Concurrency to System Design (ACSD). Xi'an, China: IEEE Computer Society, 2008, pp. 78-87.
[28]
M. Gesell, A. Morgenstern, and K. Schneider, "Lifting verification results for preemption statements," in Software Engineering and Formal Methods (SEFM). Madrid, Spain: IEEE Computer Society, 2013.
[29]
K. Schneider, Verification of Reactive Systems - Formal Methods and Algorithms, ser. Texts in Theoretical Computer Science (EATCS Series). Springer, 2003.
[30]
Y. Bai, J. Brandt, and K. Schneider, "Preservation of LTL properties in desynchronized systems," in Formal Methods and Models for Codesign (MEMOCODE), S. Shukla, L. Carloni, D. Kroening, and J. Brandt, Eds. Arlington, Virginia, USA: ACM, 2012, pp. 53-63.
- Translating synchronous guarded actions to interleaved guarded actions
Recommendations
Translating concurrent action oriented specifications to synchronous guarded actions
LCTES '10Concurrent Action-Oriented Specifications (CAOS) model the be- havior of a synchronous hardware circuit as asynchronous guarded actions at an abstraction level higher than the Register Transfer Level (RTL). Previous approaches always considered the ...
Translating concurrent action oriented specifications to synchronous guarded actions
LCTES '10: Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systemsConcurrent Action-Oriented Specifications (CAOS) model the be- havior of a synchronous hardware circuit as asynchronous guarded actions at an abstraction level higher than the Register Transfer Level (RTL). Previous approaches always considered the ...
Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions
For the design of embedded systems, many languages are in use, which are based on different models of computation such as event-, data-, and clock-driven paradigms as well as paradigms without a clear notion of time. Systems composed of such ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2013
194 pages
ISBN:9781479909056
Copyright © 2013.
Sponsors
Publisher
IEEE Computer Society
United States
Publication History
Published: 01 October 2013
Check for updates
Qualifiers
- Article
Acceptance Rates
Overall Acceptance Rate 34 of 82 submissions, 41%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 13Total Downloads
- Downloads (Last 12 months)1
- Downloads (Last 6 weeks)0
Reflects downloads up to 15 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in