A Formal Method Applied to the Automated Software Engineering with Quality Guarantees

Modern systems tend to be larger, more complex and to depend on an increasingly numerous set of requirements. In contrast, system development practices remain human-centered, depending mostly on the engineer expertise to be carried out. This paper shows how maximally permissive and deadlock-free components of software can be automatically produced. We argue that modeling methods and mathematical operations can be combined to systematically manage the software development process, based on high-level views of the system. Results show that possibly complex programming tasks become easier and independent from the expertise of the software engineer. Examples are provided to illustrate the approach.