Preview

Труды Института системного программирования РАН

Расширенный поиск

Контрактный метод спецификации реактивных требований

https://doi.org/10.15514/ISPRAS-2017-29(4)-3

Полный текст:

Аннотация

Верификация многих прикладных систем - в частности, встроенных, - включает в себя процессы, исполняющиеся во времени, для моделирования которых обычно используется временн а я логика, линейная (LTL) или ветвящаяся (CTL). Наиболее развитые автоматические доказатели программ, однако, основаны на невременн ы х теориях: например, на логике Хоара. Возможно ли все же применение этой развитой технологии верификации к более сложным системам? В качестве шага на пути к положительному ответу, мы разработали схему перевода подмножества LTL спецификаций в объектно-ориентированные программы с контрактами на языке Eiffel, которые являются естественными целями для доказателя программ AutoProof. Мы применили эту схему к опубликованной временн о й модели широко используемого реалистичного примера, авиационной системы контроля шасси, являющейся своего рода эталонной задачей для сравнения применимости различных методов спецификации. Верификация переведенной спецификации с помощью AutoProof обнаружила ошибку в одном из временн ы х свойств. Углубленное изучение данной ошибки привело к обнаружению ошибки в опубликованной абстрактной машине состояний (ASM), которая реализует переведенную модель; авторы публикации, в свою очередь, заявили об успешной верификации. Корректировка исходной спецификации и перевод результата в Eiffel с контрактами с последующей верификацией привели к успешному результату. Процесс перевода из LTL в Eiffel все еще находится в зачаточном состоянии и оптимизирован для используемого инструмента верификации (AutoProof), поэтому схема перевода не выглядит простой и элегантной. Даже с учетом указанных ограничений полученные результаты демонстрируют потенциал технологии автоматического доказательства традиционных программ в части ее применимости к специфичным проблемам встроенных систем.

Об авторах

А. Наумчев
Университет Иннополис
Россия


М. Маццара
Университет Иннополис
Россия


Б. Мейер
Университет Иннополис; Миланский технический университет; Университет Тулузы
Франция


Ж.-М. Брюэль
Университет Тулузы
Франция


Ф. Галинье
Университет Тулузы
Франция


С. Эберсоль
Университет Тулузы
Франция


Список литературы

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

Просмотров: 54


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)