VERCORS: Hardware and Software Complex for Intelligent Round-Trip Formalized Verification of Dependable Cyber-Physical Systems in a Digital Twin Environment (Position Paper)

Abstract

Formal specification, model checking and model-based testing are recommended techniques for engineering of mission-critical systems. In the meantime, those techniques struggle to obtain wide adoption due to inherent learning barrier, i.e. it is considered difficult to use those methods. There is also a common difficulty in translating the specifications in natural language, a common practice nowadays, to formal specifications. In this position paper we discuss the concept of an end-to-end methodology that helps identify specifications from various sources, automatically create formal specifications and apply them to verification of cyber-physical systems. Thus, we intent to address the challenges of creation of formal specifications in an efficient automated and tool-supported manner. The novelty of the approach is analyzed through a survey of state of the art. It is currently planned to implement this concept and evaluate it with industrial case studies.