Preview

Моделирование и анализ информационных систем

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

Операционная семантика аннотированных Reflex программ

https://doi.org/10.18255/1818-1015-2019-4-475-487

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

Аннотация

Reflex — процесс-ориентированный язык, который обеспечивает разработку простого в обслуживании управляющего программного обеспечения для программируемых логических контроллеров. Язык был успешно использован в нескольких системах управления с повышенными требованиями к надежности, например, в системе управления печью для выращивания монокристаллов кремния и в комплексе контроля радиоэлектронной аппаратуры. В настоящее время основной целью языкового проекта Reflex является разработка методов формальной верификации для Reflex программ для того, чтобы гарантировать повышенную надежность создаваемого на его основе программного обеспечения. В статье представлена формальная операционная семантика Reflex программ, расширенных аннотациями, описывающими формальную спецификацию программных требований, как необходимый базис для применения таких методов. Дан краткий обзор языка Reflex и приведен простой пример его использования — управляющая программа для сушилки рук. Определены понятия окружения и переменных, разделяемых с окружением, позволяющие абстрагироваться от конкретных портов ввода/вывода. Определены типы аннотаций, задающие ограничения на значения переменных при запуске программы, ограничения на окружение (в частности, на объект управления), инварианты цикла управления, пред- и постусловия внешних функций, используемых в Reflex программах. Аннотированный Reflex также использует стандартные аннотации assume, assert и havoc. Операционная семантика аннотированных Reflex программ использует глобальные часы и локальные часы отдельных процессов, время которых измеряется в количестве итераций цикла управления, для моделирования временных ограничений на исполнение процессов в определенных состояниях. Она хранит полную историю изменений значений разделяемых переменных для более полного описания временных свойств программы и ее окружения. Семантика учитывает бесконечность цикла выполнения программы, логику управления переходами процессов из состояния в состояние и взаимодействие процессов между собой и с окружением. Расширение формальной операционной семантики языка Reflex на аннотации упрощает доказательство корректности разрабатываемого авторами трансформационного подхода к дедуктивной верификации Reflex программ, трансформирующего аннотированную Reflex программу к аннотированной программе на сильно ограниченном подмножестве языка C, за счет сведения сложного доказательства сохранения истинности требований к программе при трансформации к более простому доказательству эквивалентности исходной и результирующей аннотированных программ относительно их операционных семантик.

Об авторе

Игорь Сергеевич Ануреев
Институт систем информатики им. А.П. Ершова СО РАН, Институт автоматики и электрометрии СО РАН
Россия
канд. физ.-мат. наук, с.н.с.


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

1. Iec, IEC, “61131-3: Programmable Controllers–Part 3: Programming Languages”, International Standard, Second Edition, International Electrotechnical Commission, Geneva, 1 (2003).

2. Basile F., Chiacchio P., Gerbasio D., “On the Implementation of Industrial Automation Systems Based on PLC”, IEEE Transactions on Automation Science and Engineering, 10:4 (2012), 990–1003.

3. Travis J., Kring J., LabVIEW for Everyone: Graphical Programming Made Easy and Fun, Third Edition, Prentice Hall PTR, Upper Saddle River, NJ, USA, 2006.

4. Zyubin V., “Using Process-Oriented Programming in LabVIEW”, Proceedings of the Second IASTED International Multi-Conference on ”Automation, Control, and Information technology“: Control, Diagnostics, and Automation. Novosibirsk, 2010, 35–41.

5. Buxton J. N., Randell B., Software Engineering Techniques: Report on a Conference Sponsored by the NATO Science Committee, NATO Science Committee, Brussels, Scientific Affairs Division, NATO, Rome, Italy, 1970.

6. Anureev I. S., Garanina N. O., Liakh T. V., Rozov A. S., Zyubin V. E., Gorlatch S., “TwoStep Deductive Verification of Control Software Using Reflex”, Preliminary Proceedings of A. P. Ershov Informatics Conference (PSI-19). Novosibirsk, Russia, Akademgorodok, Russia, July 2–5, 2019, 17–30.

7. Anureev I. S., Garanina N. O., Liakh T. V., Rozov A. S., Schulte H., Zyubin V. E., “Towards Safe Cyber-Physical Systems: the Reflex Language and its Transformational Semantics”, 14th International Siberian Conference on Control and Communications (SIBCON). Tomsk State University of Control Systems and Radioelectronics, Tomsk, April 18-20, 2019, 1–6.

8. Zyubin V. E., Liakh T. V., Rozov A. S., “Reflex Language: a Practical Notation for CyberPhysical Systems”, System Informatics, 12 (2018), 85–104.

9. Norrish M., “C Formalised in HOL”, Ph.D. thesis. University of Cambridge, Technical Report, UCAM-CL-TR-453, 1998.

10. Gurevich Y., Huggins J., “The Semantics of the C Programming Language”, International Workshop on Computer Science Logic. Lecture Notes in Computer Science, 702 (1992), 274–308.

11. Blazy S., Leroy X., “Mechanized Semantics for the Clight Subset of the C Language”, Journal of Automated Reasoning, 43:3 (2009), 263–288.

12. Nepomniaschy V. A., Anureev I. S., Mikhailov I. N., Promsky A. V., “Towards Verification of C Programs. C-light Language and its Formal Semantics”, Programming and Computer Science, 28:6 (2002), 314–323.

13. Ellison C., Rosu G., “An Executable Formal Semantics of C with Applications”, Proc. of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, 47:1 (2012), 533–544.


Для цитирования:


Ануреев И.С. Операционная семантика аннотированных Reflex программ. Моделирование и анализ информационных систем. 2019;26(4):475-487. https://doi.org/10.18255/1818-1015-2019-4-475-487

For citation:


Anureev I.S. Operational Semantics of Annotated Reflex Programs. Modeling and Analysis of Information Systems. 2019;26(4):475-487. (In Russ.) https://doi.org/10.18255/1818-1015-2019-4-475-487

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


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


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)