Рефлекс – процесс-ориентированный язык, который обеспечивает простое в сопровождении программное обеспечение для систем управления. Язык был успешно использован в нескольких критически важных с точки зрения безопасности кибер-физических системах, например в управляющем программном обеспечении для печи выращивания монокристаллического кремния. В настоящее время основной целью языкового проекта Reflex является развитие поддержки для автоматизированной разработки программного обеспечения, ориентированного на критически важные с точки зрения безопасности приложения. В данной статье представлена формальная операционная семантика языка Reflex как базис для применения формальных методов для верификации 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 plane to crash. In order to prevent this, modern planes take advantage of control software to limit the pitch angle. However, if the software is poorly designed and if system designers have forgotten that sensors might yield wrong data, the software might cause the pitch angle to become negative, so that the plane loses height and can - eventually - crash. In this paper, we investigate on a model for a Boeing passenger plane how the control software could look like. Based on our model described in MatLab/Simulink, it is easy to see based on simulation that the plane loses height when the sensor for the pitch angle provides wrong data. For the opposite case of a correctly functioning sensor, our simulation does not indicate any problems. This simulation, however, is not a guarantee that the control is indeed safe. For this reason, we translated the MatLab/Simulink-model of the controller into a hybrid program in order to make this system amenable to formal verification using the theorem prover KeYmaera
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 ontologies is their formal semantics which makes possible formal verification of described systems. Our method is based on the verification-oriented process ontology. For constructing a domain-specific process ontology, our method uses techniques of semantic markup and pattern matching to associate domain-specific concepts with classes of the process ontology. We give detailed ontological specifications of these techniques. Our method is illustrated by the example of developing a domain-specific ontology for typical elements of automatic control systems.
В Институте систем информатики СО РАН разрабатывается система C-light. Это система дедуктивной верификации C программ. Входным языком данной системы является C-light. C-light программа транслируется в C-kernel программу. Метагенератор условий корректности (УК) принимает на вход C-kernel программу и правила вывода для C-kernel. Для элиминации инвариантов циклов в системе C-light используется символический метод верификации финитных итераций. Поэтому, если C-kernel программа содержит финитную итерацию, то метагенератор порождает для нее УК, основанное на операции замены. Такая операция выражает действие цикла в символической форме. Метагенератор помечает подформулы УК семантическими метками, используя расширение метода Денни и Фишера. Если УК не удалось доказать, то система C-light генерирует его объяснение, используя семантические метки. Обратный транслятор сопоставляет строки кода промежуточной C-kernel программы и исходной C-light программы. Но в случае недоказанного УК можно попытаться доказать его ложность. Ложность УК означает несоответствие программы и спецификации. Поэтому, мы разработали и описали в данной статье эвристическую стратегию доказательства ложности УК для системы ACL2.
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 that bringing formal proof in their development can help establishing safety properties and get an efficient certification process. Other industries (e.g. aerospace, railway, nuclear) that produce critical systems requiring certification also took the path of formal verification techniques. One of these techniques is \emph{deductive proof}. It can give a higher level of confidence in proving critical safety properties and even avoid unit testing.
In this paper, we chose a production use case: a function calculating a square root by linear interpolation. We use deductive proof to prove its correctness and show the limitations we encountered with the off-the-shelf tools. We propose approaches to overcome some limitations of these tools and succeed with the proof. These approaches can be applied to similar problems, which are frequent in automotive embedded software.
Модель конечного автомата широко используется при анализе и синтезе цифровых компонентов управляющих систем. Для того чтобы учитывать временные аспекты в поведении таких систем, вводятся различные виды временных автоматов. В настоящей работе, мы исследуем проблему построения параллельной композиции автоматов с временными ограничениями и выходными задержками (выходными таймаутами). Компоненты параллельной композиции взаимодействуют в режиме диалога, и композиция выдает внешний выходной символ, когда диалог между компонентами завершается. В данной статье, мы формально определяем оператор параллельной композиции для автоматов с временными ограничениями (временных автоматов) и показываем, что в отличие от классических автоматов, наличие "медленной внешней среды" не является достаточным условием для описания параллельной композиции детерминированных временных автоматов автоматом того же класса, и таким образом, множество детерминированных автоматов с временными ограничениями не является замкнутым относительно операции параллельной композиции. В работе также рассматриваются некоторые классы детерминированных временных автоматов, замкнутые относительно этой операции.