PCS955 Model-driven Software Engineering and Reliable Software Systems

Contents and structure

Software is one of the most complex person-made artefacts and it is crucial for the proper functioning of most aspect of modern society, including critical infrastructure, health-care, business and finance, and transportation systems. Consequences of this complexity has led to many disasters and challenges in recent years, such as the ESA Ariane 5 explosion, IT-project failures, cyberattacks, and wrong diagnosis and treatment, all with huge economical cost. Among the key techniques to tame software complexity and develop reliable software are abstraction, automation, and analysis, which are the main ingredients of model-driven engineering and software verification.

Development of reliable, software-intensive systems often requires the design of models and their analysis with respect to required properties. These models serve as a foundation for design and documentation, and ideally contain sufficient details to be either directly executable or serve as input to automated code generation. With proper tools, the models can also be checked for whether they exhibit properties such as safety properties ("the value of variable x will never become negative") and liveness properties ("a request sent to a server will always be followed by a response sent back to the client"). Model-driven software engineering (MDSE) is all about increasing the emphasis on providing support for modelling activities with the aim of increasing the productivity and quality of software. It is now routinely used to develop business information systems, in network system design, for web software applications, and embedded systems. 

This course focuses on domain-specific modelling (i.e., modelling techniques tailored for a specific domain of interest), quality property specification, algorithms, tools and techniques which enable structural and behavioural modelling, automated verification, and model execution. The course covers paradigms and languages central to the specification of software structure, such as UML, Ecore, graph transformations, QVT, ATL and Diagram Predicate Framework. Specific MDSE related topics like LowCode, model version control, meta-model/model co-evolution, multilevel and deep meta-modelling are introduced. Object constraint languages, first order logic and graph constraints/predicates are introduced for specification of structural correctness properties. Model transformation and code generation through different control and execution mechanisms are covered.

For behavioural specifications, we introduce the temporal logics of LTL and CTL, and cover application of novel run-time software verification techniques. Algorithms and data structures supporting model checking are covered in conjunction with the central techniques and approaches for tackling the state explosion problem. Model-checking will be carried out with tools such as CPN Tools, the Maude rewriting logic framework, the Spin model checker, and Java Pathfinder. Examples of industrial applications of software model checking techniques are discussed.

Learning Outcome

Upon completion of the course the candidate should be able to: 

• explain the syntax and semantics of constructs underlying modelling languages for software structure and behaviour. 
• define and explain graph-based and rule-based model transformation systems. 
• explain abstract and concrete syntaxes for modelling languages and distinguish between graph-based and text-based syntaxes of models. 
• define and explain the syntax and semantics of structural constraint languages, and of linear and branching time temporal logic for expressing state- and action oriented correctness properties. 
• explain core algorithms for model transformations. 
• explain core algorithms, data structures, and paradigms for model checking based on state space exploration. 
• discuss and compare approaches for alleviating the state explosion problem in explicit state space exploration. 

Skills 

• determine proper abstraction levels for constructing software models. 
• formulate static consistency criteria for software models. 
• formulate dynamic correctness criteria for software using temporal logic. 
• use modelling tools and apply model transformation tools 
• apply tools for verification of models and their executions against constraints and behavioural properties 
• plan and conduct experimental evaluation of model transformations, model checking algorithms, and their implementation. 

General competence 

• assess the applicability and limitations of modelling and verification methods. 
• discuss and relate recent developments and research trends within model-driven software development and verification. 
• identify central scientific venues and journals within model-driven development, model checking and verification.

Entry requirements

General admission criteria for the PhD programme https://hvl.no/en/studies-at-hvl/study-programmes/2020h/phdcs/ 

Recommended previous knowledge

General software engineering curriculum such as software modeling, software development, and information modeling.

Teaching methods

The course consists of a combination of lectures, seminars and workshops. The lectures will be used for covering the core material of the course. Seminars permit participants to present and discuss recent research papers on topics in model-driven software engineering. The seminars will also be used for presentations by visiting researchers from the field. The workshops will be used for experimentation and assessment of tools and technologies supporting model-driven software engineering and software verification.

Compulsory learning activities

The course includes a number of small assignments concentrating on the application of model-driven software engineering and verification for the development of small and medium sized software systems. A larger project will be conducted by the students focusing on either theoretical development, or a case study applying empirical methods to evaluate software tools on a larger example of a software system. The results from the project must be presented in a seminar and documented in a research paper. Each participant must give at least one seminar/presentation and an oral presentation of the larger project. The small assignments and the project work (paper and presentation) must have been approved in order to take the exam. Approved compulsory assignments and project work are valid for one semester after the examination.

Assessment

The course is graded pass/fail based on an oral exam.