Рефлекс – процесс-ориентированный язык, который обеспечивает простое в сопровождении программное обеспечение для систем управления. Язык был успешно использован в нескольких критически важных с точки зрения безопасности кибер-физических системах, например в управляющем программном обеспечении для печи выращивания монокристаллического кремния. В настоящее время основной целью языкового проекта Reflex является развитие поддержки для...

During the climb flight of big passenger planes, the pilot directly adjusts the pitch elevator and the plane reacts on this by changing its pitch angle. However, if the pitch angle becomes too large, the plane is in danger of an airflow disruption on the wings, which can cause the...

User-friendly formal specification and verification of concurrent systems from various subject domains are active research topics due to their practical significance. In this paper, we present the method for development of verification-oriented domain-specific process ontologies which are used to describe concurrent systems of subject domains. One of advantages of such...

В Институте систем информатики СО РАН разрабатывается система C-light. Это система дедуктивной верификации C программ. Входным языком данной системы является C-light. C-light программа транслируется в C-kernel программу. Метагенератор условий корректности (УК) принимает на вход C-kernel программу и правила вывода для C-kernel. Для элиминации инвариантов циклов в системе C-light используется символический...

For many years, automotive embedded systems have been validated only by testing. In the near future, Advanced Driver Assistance Systems (ADAS) will take a greater part in the car’s software design and development. Furthermore, their increasing critical level may lead authorities to require a certification for those systems. We think...

Модель конечного автомата широко используется при анализе и синтезе цифровых компонентов управляющих систем. Для того чтобы учитывать временные аспекты в поведении таких систем, вводятся различные виды временных автоматов. В настоящей работе, мы исследуем проблему построения параллельной композиции автоматов с временными ограничениями и выходными задержками (выходными таймаутами). Компоненты параллельной композиции взаимодействуют...