Enabling continuous integration in a formal methods setting
- PDF / 1,057,395 Bytes
- 17 Pages / 595.276 x 790.866 pts Page_size
- 70 Downloads / 212 Views
STTT Regular Paper
Enabling continuous integration in a formal methods setting Luis Diogo Couto1 · Peter W. V. Tran-Jørgensen2 · René S. Nilsson3 · Peter Gorm Larsen2
© Springer-Verlag GmbH Germany, part of Springer Nature 2019
Abstract In modern software development, the practices of continuous integration and DevOps are widely used to increase delivery speed and reduce the time it takes to deploy software changes to production. If formal method tools cannot be efficiently integrated in a DevOps paradigm, then their impact on software development will be reduced. In this paper, we present work addressing this issue through a series of extensions for the Overture tool supporting the Vienna Development Method. These extensions enable Overture to be used in a DevOps setting, through continuous integration and validation of models and generated code via integration with the Jenkins automation server. We frame the integration of formal methods and DevOps in a series of principles, demonstrate the value of this integration through a case study, and reflect on our experiences using formal methods and DevOps in an industrial setting. We hope that this work can help other formal method practitioners integrate their tools with DevOps. Keywords VDM · Modelling · Simulation · Code generation · Test automation · Continuous integration · DevOps
1 Introduction When developing systems in industrial settings, practices such as continuous integration (CI) [14] and DevOps have become common. In order for formal methods (FMs) to effectively impact software development, it must be possible for them to integrate with such practices so that organisations working under a DevOps paradigm can leverage the benefits of FMs in an efficient way [5,6]. Indeed, FM practitioners argue that in order for FMs to effectively contribute to software development, they must be integrated in the development life-cycle [23], the principles in the agile manifesto
B
Peter W. V. Tran-Jørgensen [email protected] Luis Diogo Couto [email protected] René S. Nilsson [email protected] Peter Gorm Larsen [email protected]
1
United Technologies Research Center, Cork, Ireland
2
DIGIT, Aarhus University, Aarhus, Denmark
3
AGCO A/S, Randers, Denmark
must be considered [25] and the associated tools must support automation of the development tasks [41]. One particular challenge when using FMs under a DevOps paradigm, particularly model-based FMs, is that of dealing with software components that have not been developed using a model-based approach (for example, legacy systems). In this paper, we broadly refer to such components as external components. These components must be integrated at the modelling stage and also with the final system realisation, achieved via code generation. Furthermore, such integration should be seamless and consistent (for example, the glue code used to integrate the external component should only be written once). Finally, the approach to integrate the external components must be amenable to CI, so that we may have efficient, auto
Data Loading...
