Compilation of synchronous observers as code contracts

ABSTRACT

Synchronous languages have long been the standard formalism for modeling and implementing embedded control software in critical domains like avionics, automotive or railway system development. Those languages are equipped with qualified compilers that generate the target final embedded code. An extensively used technique to define the expected behavior is the use of synchronous observers. Those observers are typically used for simulation and testing purposes. However, the information contained in those observers is lost during the compilation process. This makes the verification of expected behavior at code level difficult, since it requires the re-specification of the observer. In this paper, we propose an integrated process in which functional properties expressed at the model level through synchronous observers are compiled as code-level contracts. We also show how these specifications, both at model level and code level could be analyzed via SMT-based model checking, static analysis and runtime verification. We have implemented these techniques in a tool chain targeting embedded systems modeled in Simulink.

References

1. DO-178B: Software considerations in airborne systems and equipment certification. Technical report, RTCA, 1992.
2. DO-178C, software considerations in airborne systems and equipment certification, 2011.
3. C. Artho, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser, and R. Washington. Combining test case generation and runtime verification. Theor. Comput. Sci., 336:209--234, 2005.
4. P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language. version 1.7. 1938
5. A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. In Proc. of the IEEE, pages 1270--1282, 1991.
6. A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. L. Guernic, R., and D. Simone. The synchronous languages 12 years later. In Proc. of the IEEE, pages 64--83, 2003.
7. D. Biernacki, J.-L. Colaço, G. Hamon, and M. Pouzet. Clock-directed modular code generation for synchronous data-flow languages. In LCTES, pages 121--130, 2008.
8. G. Brat, D. Bushnell, M. Davies, D. Giannakopoulou, F. Howar, and T. Kahsai. Verifying the safety of a flight-critical system. Technical report, NASA Ames, September 2014.
9. P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre: A declarative language for programming synchronous systems. In POPL, pages 178--188, 1987.
10. P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. Lustre: a declarative language for real-time programming. In Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, POPL '87, pages 178--188. ACM, 1987.
11. A. Champion, R. Delmas, M. Dierkes, P.-L. Garoche, R. Jobredeaux, and P. Roux. Formal methods for the analysis of critical control systems models: Combining non-linear and linear analyses. In FMICS, pages 1--16, 2013.
12. J. J. Chilenski and S. P. Miller. Applicability of modified condition/decision coverage to software testing. Software engineering, 9(5):193--200, 1994.
13. L. A. Clarke and D. S. Rosenblum. A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes, 31:25--37, 2006.
14. R. Cleaveland, S. Smolka, and S. Sims. An instrumentation-based approach to controller model validation. In M. Broy, I. Krüger, and M. Meisinger, editors, Model-Driven Development of Reliable Automotive Services, volume 4922 of LNCS, pages 84--97. Springer, 2008.
15. P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-c: a software analysis perspective. SEFM'12, pages 233--247. Springer, 2012.
16. M. Gesell and K. Schneider. A hoare calculus for the verification of synchronous languages. PLPV '12, pages 37--48. ACM, 2012.
17. G. Hagen and C. Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In FMCAD-2008, pages 109--117. IEEE, 2008.
18. N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In AMAST, pages 83--96, 1993.
19. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576--580, 1969.
20. R. M. Hueschen. Development of the Transport Class Model (TCM) aircraft simulation from a sub-scale Generic Transport Model (GTM) simulation. Technical report, NASA, Langley Research Center, 2011.
21. T. Kahsai and C. Tinelli. PKIND: a parallel k-induction based model checker. In PDMC, volume 72 of EPTCS, pages 55--62, 2011.
22. J. Rushby. The versatile synchronous observer. In SBMF, pages 1--1. Springer, 2012.
23. J. Signoles. E-ACSL: Executable ANSI/ISO C Specification Language. version 1.8.
24. A. Toom, N. Izerrouken, T. Naks, M. Pantel, and O. Ssi-Yan-Kai. Towards reliable code generation with an open tool: Evolutions of the Gene-Auto toolset. In ERTS, http://www.sia.fr, 2010. Société des Ingénieurs de l'Automobile.
25. M. Westhead and S. Nadjm-Tehrani. Verification of embedded systems using synchronous observers. In Conference on Formal Techniques in Real-time and Fault-tolerant Systems, LNCS 1135, pages 405--419. Springer, 1996.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Compilers

    • General programming languages

      • Language features

        • Concurrent programming structures

        • Constraints