Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models

摘要

This work relates to the automatic generation of logical specifications extracted directly from workflow-oriented behavioural models of software. The aim is to present a unified framework, which gives formal foundations and an algorithm for the logical specification generation process, allowing for further implementation works. Logical specifications are considered as sets of temporal logic formulas. The extraction process relies on the assumption that the entire developed model is structured purely by predefined workflow patterns. We are proposing a method to automatically transform behavioural models into logical specifications. This pattern-based feature-compositional approach, which we have denoted as Pi C, allows us to preserve the logical satisfiability, whilst guaranteeing expressiveness and naturality. Applying these concepts with user-friendly notations enables us to form a stronger link between the benefits of possessing behavioural model logical specifications, obtained automatically and on demand, with the ability to routinely analyse the developed software models in a logical style. (C) 2019 Elsevier Inc. All rights reserved.