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:

Knowledge

• has thorough knowledge of the syntax and semantics of constructs underlying modelling languages for software structure and behaviour.
• has thorough knowledge of model transformation systems.
• can define and explain the syntax and semantics of linear and branching time temporal logic for expressing state- and action oriented correctness properties.
• has thorough knowledge on core algorithms, data structures, and paradigms for model checking based on state space exploration.
• can discuss and compare approaches for alleviating the state explosion problem in explicit state space exploration.

Skills

• can apply tools for definition of models, metamodels, and model transformations
• can formulate static consistency criteria for software models
• can formulate dynamic correctness criteria for software using temporal logic
• can apply tools for verification of models and their executions against constraints and behavioural properties
• can plan and conduct experimental evaluation of model transformations, model checking algorithms, and their implementation.

General competence

• can determine proper abstraction levels for constructing software models
• can assess the applicability and limitations of modelling and verification methods.
• can discuss and relate recent developments and research trends within model-driven software development and verification.
• can identify and participate in debates in central scientific venues and journals within model-driven development, model checking and verification.

Entry requirements

General admission criteria for the PhD programme in Computer Science

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 and reliable software systems. 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 4-5 assignments in the form of practical exercises, written reports, and presentations concentrating on the application of model-driven software engineering and verification for the development of small and medium sized software systems. These assignments must have been approved in order to take the exam. Approved compulsory assignments are valid for one semester after the examination.

Assessment

Oral exam and assignment.

The course has an examination in two parts: an oral exam and a project report.

The students must conduct a project focusing on either the theoretical aspects of the course or a case study applying one or more of the topics of the course in a software system. The results from the project must be documented in a research paper.

The research paper accounts for 30% of the final grade and the oral exam accounts for 70% of the final grade.

Both parts must get a passing grade in order to get a final grade for the course.

In case one of the parts gets a failing grade, that part can be taken as a re-sitting/postponed exam.

Grading scale is pass / fail.

Examination support material

Oral exam: No support material.

Assignment (project report): All support material is permitted.

More about examination support material

Course reductions

• DAT355 - Modelldriven programvareutvikling og pålitelege programvaresystem - Reduction: 10 studypoints