Publication: Specification Language Based on Linear Temporal Logic for Automatic Construction of Statically Verified Systems
Дата
2022
Авторы
Kosikov, S.
Slieptsov, I.
Ismailova, L.
Wolfengagen, V.
Journal Title
Journal ISSN
Volume Title
Издатель
Аннотация
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.The given paper considers an approach to the construction of information systems, the interaction of which with the user can be described in the form of a small set of formal requirements. The means of formal specification are proposed in the form of a language allowing to express requirements compactly and close to how they are formulated by the developer. The language is an extension of the language of linear temporal logic. The language support tools ensure the construction of a supporting environment that is sufficient for the construction of the system and static verification of its correctness. Based on the previously proposed approach to the automatic construction of systems on the example of a model of asynchronous discrete interaction (question-answer) with the user, the paper demonstrates that a statically verifiable solution to the problem in the form of a function with a certain signature does exist. The specification language permits to identify a variety of interaction protocols that can be implemented regardless of user actions.
Описание
Ключевые слова
Цитирование
Specification Language Based on Linear Temporal Logic for Automatic Construction of Statically Verified Systems / Kosikov, S. [et al.] // Studies in Computational Intelligence. - 2022. - 1032 SCI. - P. 164-169. - 10.1007/978-3-030-96993-6_15
URI
https://www.doi.org/10.1007/978-3-030-96993-6_15
https://www.scopus.com/record/display.uri?eid=2-s2.0-85127650524&origin=resultslist
http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=Alerting&SrcApp=Alerting&DestApp=WOS_CPL&DestLinkType=FullRecord&UT=WOS:000833484200015
https://openrepository.mephi.ru/handle/123456789/28955
https://www.scopus.com/record/display.uri?eid=2-s2.0-85127650524&origin=resultslist
http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=Alerting&SrcApp=Alerting&DestApp=WOS_CPL&DestLinkType=FullRecord&UT=WOS:000833484200015
https://openrepository.mephi.ru/handle/123456789/28955