Контрактный метод спецификации реактивных требований
https://doi.org/10.15514/ISPRAS-2017-29(4)-3
Аннотация
Ключевые слова
Об авторах
А. Наумчев
Университет Иннополис
Россия
Россия
М. Маццара
Университет Иннополис
Россия
Россия
Б. Мейер
Университет Иннополис; Миланский технический университет; Университет Тулузы
Франция
Франция
Ж.-М. Брюэль
Университет Тулузы
Франция
Франция
Ф. Галинье
Университет Тулузы
Франция
Франция
С. Эберсоль
Университет Тулузы
Франция
Франция
Список литературы
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.
Рецензия
Для цитирования:
Наумчев А., Маццара М., Мейер Б., Брюэль Ж., Галинье Ф., Эберсоль С. Контрактный метод спецификации реактивных требований. Труды Института системного программирования РАН. 2017;29(4):39-54. https://doi.org/10.15514/ISPRAS-2017-29(4)-3
For citation:
Naumchev A., Mazzara M., Meyer B., Bruel J., Galinier F., Ebersold S. A contract-based method to specify stimulus-response requirements. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):39-54. https://doi.org/10.15514/ISPRAS-2017-29(4)-3
Послать статью по эл. почте 