A contract-based method to specify stimulus-response requirements

The verification of many practical systems - in particular, embedded systems - involves processes executing over time, for which it is common to use models based on temporal logic, in either its linear (LTL) or branching (CTL). Some of today’s most advanced automatic program verifiers, however, rely on non-temporal theories, particularly Hoare-style logic. Can we still take advantage of this sophisticated verification technology for more challenging systems? As a step towards a positive answer, we have defined a translation scheme from temporal specifications to contract-equipped object-oriented programs, expressed in Eiffel and hence open for processing by the AutoProof program prover. We have applied this scheme to a published CTL model of a widely used realistic example, the “landing gear” system which has been the subject of numerous competing specifications. An attempt to verify the result in AutoProof failed to prove one temporal property, which on further inspection seemed to be wrong in the original published model, even though the published work claimed to have verified an Abstract State Machine implementation of that model. Correcting the CTL specification to reflect the apparent informal attempt, re-translating again to contracted Eiffel and re-running the verification leads to success. The LTL-to-contracted-Eiffel process is still ad hoc, and tailored to generate the kind of scheme that the target verification tool (AutoProof) can handle best, rather than the simplest or most elegant scheme. Even with this limitation, the results highlight the need for rigor in the verification process, and (on the positive side) demonstrate that the highly advanced mechanized proof technology developed over several decades for the verification of traditional programs also has the potential of handling the demanding needs of embedded systems and other demanding contemporary developments.

seamless requirements, design by contract, autoproof, eiffel, landing gear system

1. J. Tschannen, C. A. Furia, M. Nordio, and N. Polikarpova, “Autoproof: Auto-active functional verification of object-oriented programs,” arXiv preprint arXiv:1501.03063, 2015.

2. B. Meyer, Touch of Class: learning to program well with objects and contracts. Springer, 2009.

3. I. J. Hayes, M. A. Jackson, and C. B. Jones, Determining the Specification of a Control System from That of Its Environment, pp. 154-169. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003.

4. E. Clarke and E. Emerson, “Design and synthesis of synchronization skeletons using branching time temporal logic,” Logics of programs, pp. 52-71, 1982.

5. P. Arcaini, A. Gargantini, and E. Riccobene, “Modeling and analyzing using asms: the landing gear system case study,” in International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 36-51, Springer, 2014.

6. F. Boniol and V. Wiels, “The landing gear system case study,” in International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 1-18, Springer, 2014.

7. R. Koymans, “Specifying real-time properties with metric temporal logic,” Real-time systems, vol. 2, no. 4, pp. 255- 299, 1990.

8. A. Naumchev and B. Meyer, “Complete contracts through specification drivers,” in 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 160-167, July 2016.

9. Y. Gurevich, “Sequential abstract-state machines capture sequential algorithms,” ACM Transactions on Computational Logic (TOCL), vol. 1, no. 1, pp. 77-111, 2000.

10. A. Naumchev, “Lgs asm ground model in eiffel.” https://github.com/anaumchev/lgs_ground_model, 2017.

11. N. Polikarpova, J. Tschannen, C. A. Furia, and B. Meyer, “Flexible invariants through semantic collaboration,” in FM 2014: Formal Methods, pp. 514-530, Springer, 2014.

12. H. Yamada, “Real-time computation and recursive functions not real-time computable,” IRE Transactions on Electronic Computers, vol. EC-11, pp. 753-760, Dec 1962.

13. M. Mazzara and A. Bhattacharyya, “On modelling and analysis of dynamic reconfiguration of dependable real time systems,” in Proceedings of the 2010 Third International Conference on Dependability, DEPEND ’10, (Washington, DC, USA), pp. 173-181, IEEE Computer Society, 2010.

14. M. Mazzara, “Timing issues in web services composition,” in Formal Techniques for Computer Systems and Business Processes, European Performance Engineering Workshop, EPEW 2005 and International Workshop on Web Services and Formal Methods, WS-FM 2005, Versailles, France, September 1-3, 2005, Proceedings, pp. 287-302, 2005.

15. L. Ferrucci, M. M. Bersani, and M. Mazzara, “An LTL semantics of business workflows with recovery,” in ICSOFTPT 2014 - Proceedings of the 9th International Conference on Software Paradigm Trends, Vienna, Austria, 2931 August, 2014, pp. 29-40, 2014.

16. M. Berger and K. Honda, “The two-phase commitment protocol in an extended pi-calculus,” Electr. Notes Theor. Comput. Sci., vol. 39, no. 1, pp. 21-46, 2000.

17. A. Iliasov, A. Romanovsky, L. Laibinis, E. Troubitsyna, and T. Latvala, “Augmenting event-b modelling with real time verification,” in Proceedings of the First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches, FormSERA ’12, 2012.

18. D. Fahland, D. Lubke, J. Mendling, H. Reijers, B. Weber,¨ M. Weidlich, and S. Zugal, Declarative versus Imperative Process Modeling Languages: The Issue of Understandability. Springer Berlin Heidelberg, 2009.

19. A. Bormotova, “Translation of natural language into hoare triples.” https://github.com/An-Dole/ Semantic-mapping.

20. V. Skukov, “Translation of hoare triples into natural language.” https://github.com/flosca/hybrid.

21. R. Gmehlich, K. Grau, F. Loesch, A. Iliasov, M. Jackson, and M. Mazzara, “Towards a formalism-based toolkit for automotive applications,” in 1st FME Workshop on Formal Methods in Software Engineering, FormaliSE 2013, San Francisco, CA, USA, May 25, 2013, pp. 36-42, 2013.