SCCharts: sequentially constructive statecharts for safety-critical applications: HW/SW-synthesis for a conservative extension of synchronous statecharts

ABSTRACT

We present a new visual language, SCCharts, designed for specifying safety-critical reactive systems. SCCharts use a statechart notation and provide determinate concurrency based on a synchronous model of computation (MoC), without restrictions common to previous synchronous MoCs. Specifically, we lift earlier limitations on sequential accesses to shared variables, by leveraging the sequentially constructive MoC. The semantics and key features of SCCharts are defined by a very small set of elements, the Core SCCharts, consisting of state machines plus fork/join concurrency. We also present a compilation chain that allows efficient synthesis of software and hardware.

References

1. J. Aguado, M. Mendler, R. von Hanxleden, and I. Fuhrmann. Grounding synchronous deterministic concurrency in sequential programming. In Proceedings of the 23rd European Symposium on Programming (ESOP'14), LNCS 8410, pages 229--248, Grenoble, France, Apr. 2014. Springer.
2. C. André. Semantics of SyncCharts. Technical Report ISRN I3S/RR-2003-24-FR, I3S Laboratory, Sophia-Antipolis, France, April 2003.
3. A. W. Appel. SSA is functional programming. SIGPLAN Not., 33(4): 17--20, Apr. 1998. ISSN 0362-1340.
4. A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. L. Guernic, and R. de Simone. The Synchronous Languages Twelve Years Later. In Proc. IEEE, Special Issue on Embedded Systems, volume 91, pages 64--83, Piscataway, NJ, USA, Jan. 2003. IEEE.
5. G. Berry. The foundations of Esterel. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language, and Interaction: Essays in Honour of Robin Milner, pages 425--454, Cambridge, MA, USA, 2000. MIT Press. ISBN 0-262-16188-5.
6. P. Caspi, J.-L. Colaço, L. Gérard, M. Pouzet, and P. Raymond. Synchronous Objects with Scheduling Policies: Introducing safe shared memory in Lustre. In ACM Int'l Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES'09), pages 11--20, Dublin, Ireland, June 2009. ACM.
7. J.-L. Colaço, B. Pagano, and M. Pouzet. A conservative extension of synchronous data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT'05), pages 173--182, New York, NY, USA, Sept. 2005. ACM.
8. J.-L. Colaço, G. Hamon, and M. Pouzet. Mixing signals and modes in synchronous data-flow systems. In ACM International Conference on Embedded Software (EMSOFT'06), pages 73--82, Seoul, South Korea, Oct. 2006. ACM.
9. S. A. Edwards. Tutorial: Compiling concurrent languages for sequential processors. ACM Transactions on Design Automation of Electronic Systems, 8(2):141--187, Apr. 2003.
10. J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems, 9(3):319--349, 1987. ISSN 0164-0925.
11. H. Fuhrmann and R. von Hanxleden. On the pragmatics of model-based design. In Foundations of Computer Software. Future Trends and Techniques for Development---15th Monterey Workshop 2008, Budapest, Hungary, September 24--26, 2008, Revised Selected Papers, volume 6028 of LNCS, pages 116--140, 2010..
12. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE, 79(9):1305--1320, Sept. 1991.
13. P. B. Hansen. Java's insecure parallelism. SIGPLAN Not., 34(4):38--45, Apr. 1999. ISSN 0362-1340.
14. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231--274, June 1987.
15. D. Harel and A. Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4): 293--333, Oct. 1996.
16. E. A. Lee. The problem with threads. IEEE Computer, 39(5):33--42, 2006.
17. J. Lukoschus and R. von Hanxleden. Removing cycles in Esterel programs. EURASIP Journal on Embedded Systems, Special Issue on Synchronous Paradigms in Embedded Systems, 2007. Article ID 48979, 23 pages.
18. F. Maraninchi. The Argos language: Graphical representation of automata and description of reactive systems. In IEEE Workshop on Visual Languages, Oct. 1991.
19. R. Milner. Communication and Concurrency. Prentice Hall, 1989.
20. D. Potop-Butucaru, S. A. Edwards, and G. Berry. Compiling Esterel. Springer, May 2007.
21. S. Prochnow, C. Traulsen, and R. von Hanxleden. Synthesizing Safe State Machines from Esterel. In Proceedings of ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES'06), Ottawa, Canada, June 2006.
22. T. Reenskaug. Models -- Views -- Controllers, Dec. 1979. Xerox PARC technical note.
23. C. Schneider, M. Spönemann, and R. von Hanxleden. Just model! -- Putting automatic synthesis of node-link-diagrams into practice. In Proceedings of the IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC'13), pages 75--82, San Jose, CA, USA, 15--19 Sept. 2013..
24. K. Schneider. Embedding imperative synchronous languages in interactive theorem provers. In Conference on Application of Concurrency to System Design (ACSD), pages 143--156, Newcastle upon Tyne, UK, June 2001. IEEE Computer Society.
25. J. T. Schwartz. Ultracomputers. ACM Trans. Program. Lang. Syst., 2 (4):484--521, Oct. 1980.
26. T. R. Shiple, G. Berry, and H. Touati. Constructive Analysis of Cyclic Circuits. In Proc. European Design and Test Conference (ED&TC'96), Paris, France, pages 328--333, Los Alamitos, California, USA, Mar. 1996. IEEE Computer Society Press.
27. O. Tardieu. Goto and concurrency---introducing safe jumps in Esterel. In Proceedings of Synchronous Languages, Applications, and Programming (SLAP'04), Barcelona, Spain, Mar. 2004.
28. O. Tardieu and R. de Simone. Curing schizophrenia by program rewriting in Esterel. In Proceedings of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'04), San Diego, CA, USA, 2004.
29. C. Traulsen, T. Amende, and R. von Hanxleden. Compiling SyncCharts to Synchronous C. In Proceedings of the Design, Automation and Test in Europe Conference (DATE'11), pages 563--566, Grenoble, France, Mar. 2011. IEEE.
30. M. von der Beeck. A comparison of Statecharts variants. In H. Langmaack, W. P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of LNCS, pages 128--148. Springer-Verlag, 1994.
31. R. von Hanxleden. SyncCharts in C---A Proposal for Light-Weight, Deterministic Concurrency. In Proc. Int'l Conference on Embedded Software (EMSOFT'09), pages 225--234, Grenoble, France, Oct. 2009. ACM.
32. R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer, and O. O'Brien. SCCharts: Sequentially Constructive Statecharts for safety-critical applications. Technical Report 1311, Christian-Albrechts-Universität zu Kiel, Department of Computer Science, Dec. 2013. ISSN 2192-6247.
33. R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, O. O'Brien, and P. Roop. 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, 2014. To appear.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Compilers

    • General programming languages

      • Language features

        • Concurrent programming structures