Automated Derivation of Formal Properties from Requirements

Early detection of design errors in the life cycle of systems is one of the many benefits one may expect from using an model-based systems engineering approach. The formal verification of models is thus an issue. Among verification techniques, the paper focuses on model checking. Taking as input a set of properties and a model, model checking outputs a 'yes/no' answer for each property saying whether the property is verified or not. The relevance of this proof relies on the relevance of the defined properties. The paper proposes solutions for automated generation of properties from a SysML model and, more specifically, from the requirements expressed in the SysML model. We introduce an AI- and syntactic rule-based process that assists systems engineers in the generation of syntactically correct CTL properties, along with complementary contributions for computing and propagating requirement coverage from formal verification results, backtracing them directly in the SysML requirement diagram. The approach is mathematically defined, with explanatory comments accompanying the formalism to support comprehension. The proposed approach is further implemented by the free software TTool-AI. The latter is an open source SysML toolkit extended with an LLM-based assistant. A satellite system and an embedded maritime system serve as case studies.