Closing the gap between the specification and the implementation: the ASMETA way

In software system development, formal models are used to precisely specify the initial requirements, understand what the system is supposed to do and prove properties of the system. Ideally, formal specifications should be developed long before the system is implemented, and in a model-driven software development the code would be automatically generated from the models. However, quite often either code generation is not available or not reliable enough, or the final specification of a system becomes ready only together with (or even after) its implementation. In all these cases, the conformance relation between the formal specification and the concrete implementation must be checked, in order to assure that the software behaves as expected. In this paper, we show how the ASMETA framework, based on the use of the Abstract State Machine (ASM) formal method, can be used to assist the developer in the conformance checking of Java code against ASM models. We present a technique to formally link a Java class with its ASM formal specification, and two approaches for checking their conformance: offline (i.e., before deployment) using model-based test generation, and online (i.e., after deployment) using runtime verification. We also report our experience in applying these two techniques in the context of safety critical systems, where conformance checking of the implementation against its formal specification is highly demanded.