On the impact of rigorous approaches on the quality of development

Software systems are expanding and becoming increasingly present in everyday activities. The constantly evolving society demands that they deliver more functionality, are easy to use and work as expected. All these challenges increase the size and complexity of a system. People may not be aware of a presence of a software system, until it malfunctions or even fails to perform. The concept of being able to depend on the software is particularly significant when it comes to the critical systems. At this point quality of a system is regarded as an essential issue, since any deficiencies may lead to considerable money loss or life endangerment. Traditional development methods may not ensure a sufficiently high level of quality. Formal methods, on the other hand, allow us to achieve a high level of rigour and can be applied to develop a complete system or only a critical part of it. Such techniques, applied during system development starting at early design stages, increase the likelihood of obtaining a system that works as required. However, formal methods are sometimes considered difficult to utilise in traditional developments. Therefore, it is important to make them more accessible and reduce the gap between the formal and traditional development methods. This thesis explores the usability of rigorous approaches by giving an insight into formal designs with the use of graphical notation. The understandability of formal modelling is increased due to a compact representation of the development and related design decisions. The central objective of the thesis is to investigate the impact that rigorous approaches have on quality of developments. This means that it is necessary to establish certain techniques for evaluation of rigorous developments. Since we are studying various development settings and methods, specific measurement plans and a set of metrics need to be created for each setting. Our goal is to provide methods for collecting data and record evidence of the applicability of rigorous approaches. This would support the organisations in making decisions about integration of formal methods into their development processes. It is important to control the software development, especially in its initial stages. Therefore, we focus on the specification and modelling phases, as well as related artefacts, e.g. models. These have significant influence on the quality of a final system. Since application of formal methods may increase the complexity of a system, it may impact its maintainability, and thus quality. Our goal is to leverage quality of a system via metrics and measurements, as well as generic refinement patterns, which are applied to a model and a specification. We argue that they can facilitate the process of creating software systems, by e.g. controlling complexity and providing the modelling guidelines. Moreover, we find them as additional mechanisms for quality control and improvement, also for rigorous approaches. The main contribution of this thesis is to provide the metrics and measurements that help in assessing the impact of rigorous approaches on developments. We establish the techniques for the evaluation of certain aspects of quality, which are based on structural, syntactical and process related characteristics of an early-stage development artefacts, i.e. specifications and models. The presented approaches are applied to various case studies. The results of the investigation are juxtaposed with the perception of domain experts. It is our aspiration to promote measurements as an indispensable part of quality control process and a strategy towards the quality improvement.

Programvarusystem expanderar och blir allt mer närvarande i vårt dagliga liv. Eftersom vårt samhälle är under ständig utveckling, krävs att dessa system levererar mer funktionalitet, är lätta att använda och fungerar som väntat. Alla dessa utmaningar ökar deras storlek och komplexitet. Folk är kanske inte ens medvetna om att ett programvarusystem finns förrän det inte fungerar eller misslyckas med att utföra sina uppgifter. Speciellt när det gäller kritiska system är det särskilt viktigt att kunna lita på programvaran. På denna punkt är systemets kvalitet att betraktas som en central fråga, eftersom eventuella brister kan leda till stora finansiella förluster eller risk för liv. Traditionella utvecklingsmetoder är ingen garanti för en tillräckligt hög kvalitet. Formella metoder, å andra sidan, ger oss möjlighet att uppnå en hög grad av stringens och kan tillämpas för att utveckla kompletta system eller bara kritiska delar av dem. Om den sortens tekniker tillämpas vid systemutveckling, med början redan tidigt i designfasen, ökar sannolikheten för att det resulterande systemet fungerar enligt givna krav. Formella metoder uppfattas dock ibland som svåra att använda i traditionell programvaruutveckling. Därför är det viktigt att göra dem mer tillgängliga och minska gapet mellan formella och traditionella utvecklingsmetoder. Denna avhandling undersöker användbarheten av rigorösa metoder genom att ge en inblick i formella konstruktioner med hjälp av grafisk notation. Begripligheten hos formell modellering förbättras tack vare av en kompakt representation av beslut som berör utveckling och design. Det centrala målet med avhandlingen är att undersöka vilken inverkan rigorösa metoder har på kvaliteten hos det utvecklade systemet. Detta innebär att det är nödvändigt att fastställa vissa tekniker för utvärdering av rigorös utveckling. Eftersom vi studerar olika utvecklingsmiljöer och metoder, behöver vi fastställa särskilda mätplaner och en uppsättning mätmetoder behöver skapas för varje sammanhang. Vårt mål är att ge metoder för datainsamling och samla in bevis för tillämpbarheten hos rigorösa metoder. Detta kan ge organisationer stöd i beslutsfattandet om integrering av formella metoder i sina utvecklingsprocesser. Det är viktigt att kontrollera utvecklingen av programvara, särskilt i inledningsskedet. Därför fokuserar vi på specifikations- och modelleringsfaserna, samt därtill hörande artefakter, som t.ex. modeller. Dessa har en betydande inverkan på det slutliga systemets kvalitet. Eftersom bruk av formella metoder kan öka systemets komplexitet, kan även dess underhåll påverkas, och därmed också dess kvalitet. Vårt mål är att öka systemets kvalitet via mätmetoder och mätningar, samt även genom allmänna mönster för precisering, som tillämpas på modeller och specifikationer. Vi hävdar att de kan underlätta processen att skapa programvarusystem, t.ex. genom att kontrollera komplexitet och ge modelleringsriktlinjer. Dessutom anser vi dem vara kompletterande mekanismer för kvalitetskontroll och förbättring, även för rigorösa tillvägagångssätt. Det viktigaste resultatet av denna avhandling är att tillhandahålla mätmetoder och mätningar som hjälper att utvärdera effekten av rigorösa tillvägagångssätt inom systemutveckling. Vi skapar och presenterar metoder för utvärdering av vissa kvalitetsaspekter, som bygger på strukturella, syntaktiska och processrelaterade egenskaper hos tidiga utvecklingsartefakter, dvs. specifikationer och modeller. De presenterade metoderna tillämpas på olika fallstudier. Undersökningens resultat jämförs med domänexperters uppfattning. Det är vår ambition att förespråka mätningar som en oersättelig del av kvalitetskontrollen och en strategi för kvalitetsförbättring.