Formal verification of an industrial UML-like model using mCRL2 (extended version)
Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.
Code (0)
등록된 구현이 없습니다.
Tasks
TranslationSimilar Papers 제목 키워드 기반
Performance Limits for Signals of Opportunity-Based Navigation
This paper investigates the potential of non-terrestrial and terrestrial signals of opportunity (SOOP) for navigation applications. Non-terrestrial SOOP analysis employs modified Cram\`er-Rao lower bound (MCRLB) to estab…
Learning Deep Feature Correspondence for Unsupervised Anomaly Detection and Segmentation
Developing machine learning models that can detect and localize the unexpected or anomalous structures within images is very important for numerous computer vision tasks, such as the defect inspection of manufactured pro…
Anomaly DetectionUnsupervised Anomaly DetectionAutomated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. During the program optimisation process, it w…
NegationTranslationRate Loss due to Beam Cusping in Grid of Beams
We present mean communication rate loss (MCRL) values due to the beam cusping phenomenon inherent to grid of beams based wireless systems, which are widely used/proposed in millimeter-wave and sub-THz bands. We consider …
Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach
Formally verifying audio classification systems is essential to ensure accurate signal classification across real-world applications like surveillance, automotive voice commands, and multimedia content management, preven…
Audio ClassificationClassificationManagement