An overview of research with Slco on seamless integration of formal verification into model-driven software engineering

In 2009, the Simple Language of Communicating Objects (SLCO) Domain-Specific Language was designed. Since then, a range of tools have been developed around this language to conduct research on a wide range of topics, all related to the construction of complex, component-based software, with formal verification being applied in every development step. This addresses our vision that formal verification should be seamlessly integrated into Model-Driven Software Engineering, to effectively develop correct software. In this article, we present this range of topics, and draw connections between the various, at first glance disparate, research results. We discuss the current status of the SLCO framework, i.e., the language in combination with the tools, related work w.r.t. each of the topics, and plans for future work.