More Web Proxy on the site http://driver.im/

research-article

Synthesizing manually verifiable code for statecharts

Authors:

Christian Motika,

Reinhard von HanxledenAuthors Info & Claims

REBLS 2018: Proceedings of the 5th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems

Pages 1 - 10

https://doi.org/10.1145/3281278.3281283

Published: 04 November 2018 Publication History

Abstract

Statecharts are an established mechanism to model reactive, state-oriented behavior of embedded systems. We here present an approach to automatically generate code from statecharts, with a particular focus on readability and ease of matching the generated code with the original model. This not only saves programming effort and reduces the error rate compared to manual coding, but it also facilitates the task of verifying that the code does what it is supposed to do. We have implemented this approach for the SCCharts language in an open-source framework. A user study confirmed that the generated code tends to be more readable than code from other code generators.

References

[1]

Sidharta Andalam, Partha S. Roop, and Alain Girault. 2010. Deterministic, predictable and light-weight multithreading using PRET-C. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE’10) . Dresden, Germany, 1653–1656.

Digital Library

[2]

Charles André. 2004. Computing SyncCharts Reactions. Electr. Notes Theor. Comput. Sci. 88 (2004), 3–19.

Digital Library

[3]

Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. 2003. The Synchronous Languages Twelve Years Later. In Proc. IEEE, Special Issue on Embedded Systems, Vol. 91. IEEE, Piscataway, NJ, USA, 64–83.

[4]

Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. 2017. SCADE 6: A formal language for embedded critical software development (invited paper). In 11th International Symposium on Theoretical Aspects of Software Engineering TASE . Sophia Antipolis, France, 1–11.

[5]

Gregory H. Cooper and Shriram Krishnamurthi. 2006. Embedding Dynamic Dataflow in a Call-by-Value Language. In 15th European Symposium on Programming (ESOP ’06) . Vienna, Austria, 294–308.

Digital Library

[6]

Bruce Powel Douglass. 1999. UML Statecharts. Embedded Systems Programming (Jan. 1999), 22–42.

[7]

Harald Fecher, Jens Schönborn, Marcel Kyas, and Willem P. de Roever. 2005. 29 New Unclarities in the Semantics of UML 2.0 State Machines. In ICFEM (LNCS), Vol. 3785. Springer, 52–65.

Digital Library

[8]

Insa Fuhrmann, David Broman, Reinhard von Hanxleden, and Alexander Schulz-Rosengarten. 2016. Time for Reactive System Modeling: Interactive Timing Analysis with Hotspot Highlighting. In Proceedings of the 24th International Conference on Real-Time Networks and Systems (RTNS ’16) . ACM, New York, NY, USA, 289–298.

Digital Library

[9]

Grégoire Hamon. 2005. A denotational semantics for Stateflow. In EMSOFT’05: Proceedings of the 5th ACM International Conference on Embedded Software . ACM Press, New York, NY, USA, 164–172.

Digital Library

[10]

David Harel. 1987. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8, 3 (June 1987), 231–274.

Digital Library

[11]

Les Hatton. 1995. Safer C: Developing Software for in High-Integrity and Safety-Critical Systems . McGraw-Hill, Inc.

Digital Library

[12]

Edward A. Lee. 2006. The Problem with Threads. IEEE Computer 39, 5 (2006), 33–42.

Digital Library

[13]

Michael Mendler, Reinhard von Hanxleden, and Claus Traulsen. 2009. WCRT Algebra and Interfaces for Esterel-Style Synchronous Processing. In Proceedings of the Design, Automation and Test in Europe Conference (DATE ’09) . Nice, France.

Digital Library

[14]

MISRA. 2013. MISRA C:2012: Guidelines for the Use of the C Language in Critical Systems . Motor Industry Research Association.

[15]

Christian Motika. 2017. SCCharts—Language and Interactive Incremental Implementation . Number 2017/2 in Kiel Computer Science Series. Department of Computer Science. Dissertation, Faculty of Engineering, Christian-Albrechts-Universität zu Kiel.

[16]

Dumitru Potop-Butucaru, Stephen A. Edwards, and Gérard Berry. 2007. Compiling Esterel . Springer.

Digital Library

[17]

Leanna Rierson. 2013. Developing Safety-Critical Software: A Practical Guide for Aviation Software and DO-178C Compliance . Taylor & Francis Inc.

[18]

Miro Samek. 2008. Practical UML Statecharts in C/C++Event-Driven Programming for Embedded Systems . Newnes.

Digital Library

[19]

Francisco Sant’Anna, Roberto Ierusalimschy, Noemi de La Rocque Rodriguez, Silvana Rossetto, and Adriano Branco. 2017. The Design and Implementation of the Synchronous Language CÉU. ACM Trans. Embedded Comput. Syst. 16, 4 (2017), 98:1–98:26.

Digital Library

[20]

Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Frédéric Mallet, Robert de Simone, and Julien Deantoni. 2018. Time in SCCharts. In Proc. Forum on Specification and Design Languages (FDL ’18). Munich, Germany.

[21]

Steven Smyth, Stephan Lenga, and Reinhard von Hanxleden. 2016. Model Extraction for Legacy C Programs with SCCharts. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA ’16), Doctoral Symposium (Electronic Communications of the EASST), Vol. 74. Corfu, Greece. With accompanying poster .

[22]

Michael von der Beeck. 1994. A Comparison of Statecharts Variants. In Formal Techniques in Real-Time and Fault-Tolerant Systems (LNCS), H. Langmaack, W. P. de Roever, and J. Vytopil (Eds.), Vol. 863. SpringerVerlag, 128–148.

Digital Library

[23]

Reinhard von Hanxleden. 2009. SyncCharts in C—A Proposal for Light-Weight, Deterministic Concurrency. In Proc. Int’l Conference on Embedded Software (EMSOFT ’09) . ACM, Grenoble, France, 225–234.

Digital Library

[24]

Reinhard von Hanxleden, Björn Duderstadt, Christian Motika, Steven Smyth, Michael Mendler, Joaquín Aguado, Stephen Mercer, and Owen O’Brien. 2014. SCCharts: Sequentially Constructive Statecharts for Safety-Critical Applications. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14) . ACM, Edinburgh, UK, 372–383.

Digital Library

[25]

Reinhard von Hanxleden, Michael Mendler, Joaquín Aguado, Björn Duderstadt, Insa Fuhrmann, Christian Motika, Stephen Mercer, Owen O’Brien, and Partha Roop. 2014. Sequentially Constructive Concurrency—A Conservative Extension of the Synchronous Model of Computation. ACM Transactions on Embedded Computing Systems, Special Issue on Applications of Concurrency to System Design 13, 4s (July 2014), 144:1–144:26.

Digital Library

Cited By

Grimm LSmyth SSchulz-Rosengarten Avon Hanxleden RPouzet M(2024)From Lustre to Graphical Models and SCChartsACM Transactions on Embedded Computing Systems10.1145/354497323:5(1-28)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.1145/3544973
Boysen ASchulz-Rosengarten Avon Hanxleden R(2020)A Hard Real Time Demonstrator for Dynamic Ticks and Timed SCCharts2020 Forum for Specification and Design Languages (FDL)10.1109/FDL50818.2020.9232943(1-8)Online publication date: 15-Sep-2020
https://doi.org/10.1109/FDL50818.2020.9232943

Index Terms

Synthesizing manually verifiable code for statecharts
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Source code generation

Recommendations

Propositional Statecharts for Agent Interaction Protocols

Current representations of interaction protocols either concentrate on ease of understanding and neglect the need to specify protocols unambiguously (e.g. [B. Bauer, J.P. Muller, J.Odell, Agent UML: A Formalism for Specifying Multiagent Software Systems,...
Executable object modeling with statecharts
ICSE '96: Proceedings of the 18th international conference on Software engineering

This paper reports on an effort to develop an integrated set of diagrammatic languages for modeling object-oriented systems, and to construct a supporting tool. The goal is for models to be intuitive and well-structured, yet fully executable and ...
Are Statecharts Finite Automata?
CIAA '09: Proceedings of the 14th International Conference on Implementation and Application of Automata

Statecharts, which have been introduced by D. Harel in 1987, provide compact and expressive visual formalisms for reactive systems. They have been widely used as a modeling tool and adopted by Unified Modeling Language (UML) as an important technique to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

REBLS 2018: Proceedings of the 5th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems

November 2018

70 pages

ISBN:9781450360708

DOI:10.1145/3281278

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 November 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '18

Sponsor:

SIGPLAN

SPLASH '18: Conference on Systems, Programming, Languages, and Applications: Software for Humanity

November 4, 2018

MA, Boston, USA

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
72
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Grimm LSmyth SSchulz-Rosengarten Avon Hanxleden RPouzet M(2024)From Lustre to Graphical Models and SCChartsACM Transactions on Embedded Computing Systems10.1145/354497323:5(1-28)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.1145/3544973
Boysen ASchulz-Rosengarten Avon Hanxleden R(2020)A Hard Real Time Demonstrator for Dynamic Ticks and Timed SCCharts2020 Forum for Specification and Design Languages (FDL)10.1109/FDL50818.2020.9232943(1-8)Online publication date: 15-Sep-2020
https://doi.org/10.1109/FDL50818.2020.9232943

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents