Search programme

​Use the search function to search amongst programmes at Chalmers. The programme overview and the programme syllabus relating to your studies are generally from the academic year you began your studies.

​​​

Syllabus for

Academic year
TDA291 - Software engineering using formal methods
 
Owner: DCMAS
4,0 Credits (ECTS 6)
Grading: TH - Five, Four, Three, Not passed
Level: A
Department: 0701 - Datavetenskap DI CTH/GU


Teaching language: English

Course module   Credit distribution   Examination dates
Sp1 Sp2 Sp3 Sp4 No Sp
0101 Examination 4,0 c Grading: TH   4,0 c   08 Mar 2004 pm M,  12 Jan 2004 am M,  20 Aug 2004 am V  

In programs

TITEA INFORMATION ENGINEERING, Year 3 (elective)
TDATA COMPUTER SCIENCE AND ENGINEERING, Year 3 (elective)
TDATA COMPUTER SCIENCE AND ENGINEERING - Computer Languages, Year 4 (elective)
TDATA COMPUTER SCIENCE AND ENGINEERING - Engineering of Computer-Based Systems, Year 4 (elective)
DCMAS MSc PROGR IN DEPENDABLE COMPUTER SYSTEMS, Year 1 (compulsory)
TELTA ELECTRICAL ENGINEERING, Year 4 (elective)

Examiner:




  Go to Course Homepage

Eligibility:

For single subject courses within Chalmers programmes the same eligibility requirements apply, as to the programme(s) that the course is part of.

Course specific prerequisites

Some course in programming. One of the courses Discrete mathematics (TMA965) or Mathematical logic (TMA240) is recommended.

Aim

The aim of the course is to introduce some industrially applied methods for specification and verification of programs. The course covers the design and verification of programs at two quite different levels of abstraction: the automatic verification of synchronous control programs and the development of more general programs by refinement from high level specifications. We present both the theory and the practice of those methods. We aim to convey the possibilities and the limitations of formal methods in software development.

Content

Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigour. The purpose is to construct, with high confidence, systems that behave according to their specification. The course will focus on two particular styles of formal methods for software: automatic and interactive methods. Each style will be introduced using a particular concrete tool for developing software in that style.

The automatic style inherently places restrictions on the kind of software that can be developed. The particular tool for the automatic style has not been decided upon yet. Previous years have used the synchronous programming language Lustre (*); an alternative is the SLAM (*) tool developed by Microsoft Research. Both tools make use of automatic so-called model checking methods to show that programs behave as they should.

The KeY (*) tool is an integrated tool for object-oriented design and formal verification. It is developed here at Chalmers and at the University of Karlsruhe. The target language of KeY is a subset of Java. KeY supports UML class diagrams, formal specification in OCL, translation from OCL into logic, and an interactive theorem prover that is used to formally verify statements about specifications and programs.

Familiarity with Java, UML, and predicate logic (first-order logic) is strongly encouraged. For the latter, we recommend the course "discrete mathematics", or the course "mathematical logic".

(*) URLs:
Key: http://i12www.ira.uka.de/~key/
Slam: http://research.microsoft.com/slam/
Lustre: http://www-verimag.imag.fr/SYNCHRONE/

Organisation

We will have two lectures a week, introducing formal methods in general, and the technical and theoretical concepts behind the presented methods and tools. Some lectures will contain hands-on exercises. The students will perform practical case studies using the tools in lab assignments.

Literature

The course homepage will contain papers on the various topics. There will also be lecture notes with exercises and a manual for the KeY system. All is freely available. There is no course book.

Examination

You need to complete several labs sucessfully, which together will comprise a full case study. You can do this in groups. In addition, we plan an oral or written exam at the end of the course. The grade scale is U, 3, 4, 5.


Page manager Published: Thu 03 Nov 2022.