The ICT challenge for the Allegio project is to increase the rate of innovation of complex industrial software by improving the software development process. The main emphasis is on finding faults as early as possible in the development process, especially by using modeling techniques. This includes both design models, that are part of the design flow and which ultimately results in code, and analysis models that evaluate certain aspects, such as performance or correctness. An important challenge is to combine these two types of models in the development process and obtain a smooth integration of, for instance, performance analysis and formal verification. Another challenge is to incorporate model-based testing techniques based on design models. A mapping of the main techniques to the classical V-model of software development is depicted in this figure.
The challenges mentioned above are motivated by the observation that many companies spend too much time on the software development process. Often there is a very long test and integration phase where many faults have to be corrected and non-functional properties, like safety and performance, have to be established. Although there are many academic methods which address our challenges, their incorporation in industrial practice is far from trivial and often requires new research. For instance, scalability is a well-known problem; many methods work well on small examples but the application to real world systems with millions of lines of code leads to new challenges. Given the hundreds of man years invested in existing software archives, it is highly unlikely (because of cost and risk) that the software can be redesigned from scratch. Another blocking factor is that it is difficult to integrate these techniques in a coherent development process.
The first project results concern the industrial usage of the ASD (Analytical Software Design) approach of the company Verum. This approach combines design models, from which code can be generated, with formal analysis. A detailed study of a number of industrial projects show a strong reduction in the number of defects found during testing. The approach, however, is limited to data-independent control components and a fixed set of properties. To extend the verification possibilities a combination with the timed model checker Uppaal has been made. During the application of ASD it became clear that unambiguous requirements and a stable architecture are a prerequisite for ASD. Hence, we have proposed techniques to clarify and improve requirements and reference architectures using executable models. Finally, a combination of design and analysis models has been proposed using Domain Specific Languages (DSLs). Early fault detection on the DSL level, has been obtained by a transformation from the DSL to an SMT solver which can check properties. This makes it possible to detect certain faults automatically.