Sök i programutbudet

Använd sökfunktionen för att leta efter kurser och program i Chalmers utbildningsutbud. Den programplan och utbildningsplan som avser dina studier är i allmänhet från det läsår du började dina studier.

​​​​​​​​​​​​​

Kursplan för

Läsår
TDA293 - Software engineering using formal methods
 
Kursplanen fastställd 2012-02-18 av programansvarig (eller motsvarande)
Ägare: MPALG
7,5 Poäng
Betygskala: TH - Fem, Fyra, Tre, Underkänt
Utbildningsnivå: Avancerad nivå
Huvudområde: Datateknik, Informationsteknik
Institution: 37 - DATA- OCH INFORMATIONSTEKNIK


Undervisningsspråk: Engelska
Sökbar för utbytesstudenter
Blockschema: B

Modul   Poängfördelning   Tentamensdatum
Lp1 Lp2 Lp3 Lp4 Sommarkurs Ej Lp
0110 Laboration 2,5 hp Betygskala: UG   2,5 hp    
0210 Tentamen 5,0 hp Betygskala: TH   5,0 hp   26 Okt 2012 em H,  Kontakta examinator

I program

TKITE INFORMATIONSTEKNIK, CIVILINGENJÖR, Årskurs 3 (valbar)
MPSOF SOFTWARE ENGINEERING, MSC PROGR, Årskurs 2 (valbar)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Årskurs 1 (obligatoriskt valbar)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Årskurs 2 (valbar)

Examinator:

Professor  Reiner Hähnle
Docent  Wolfgang Ahrendt


Ersätter

TDA291   Software engineering using formal methods TDA292   Software engineering using formal methods

Kursutvärdering:

http://document.chalmers.se/doc/c4651f7c-07d1-4073-8e0a-ae304903277c


  Gå till kurshemsida

Behörighet:

För kurser inom Chalmers utbildningsprogram gäller samma behörighetskrav som till de(t) program kursen ingår i.

Kursspecifika förkunskaper

Skills in object-oriented programing (like Java) are a prerequisite and skills in concurrent programming is an advantage. The course is self-contained, however, a certain maturity in mathematical methods is required, comparable to the admission criteria of the MPALG Masters programme. Alternatively, one of the courses "Logic in computer science" (DAT060) or "Testing, debugging and verification" (TDA 566) is a suitable preparation.

Syfte

The aim of this course is to introduce students to the two most important styles of formal methods for reasoning about software: automatic and interactive methods. Each style will be introduced using a particular concrete tool for developing software in that style.

Lärandemål (efter fullgjord kurs ska studenten kunna)

    * express safety properties of (concurrent) programs in a formal way.
    * describe the basics of verifying safety properties via model checking.
    * use tools which integrate and automate the model checking of safety properties.
    * write formal specifications of object-oriented system units. Understanding the concepts of method contract, class invariant, and behavioural subtyping.
    * describe how the connection between programs and formal specifications can be represented in a program logic.
    * differentiate between syntax, semantics, and calculus in connection with logic-based systems.
    * verify functional properties of simple Java programs with a verification tool.

Innehåll

Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigor. The purpose is to construct, with high confidence, systems that behave according to their specification.
The course introduces practically and theoretically the two most important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced using a concrete tool. On the model checking side, the advantage of an automated method at the same time places restrictions on the kind of properties that can be verified. Accordingly, we concentrate on the verification of safety properties. The lectures cover the following topics:

    * Theoretical foundations of model checking.
    * Property languages and their usage.
    * Performing automated verification with a software model checking tool.

For the deductive verification side, we use KeY, an integrated tool for the formal specification and verification of Java programs. The tool, which is partly developed at Chalmers and University of Gothenburg, supports formal specification in the Java Modeling Language (JML), and translation from JML into logic. An interactive theorem prover is used to formally verify statements about specifications and programs. The lectures cover the following topics:

    * Java Modeling Language (JML)
    * Formal Semantics of Systems
    * Predicate Logic for Specification of Java Programs
    * Translating JML into Dynamic Logic
    * Verifying Proof Obligations

Organisation

There are two lectures each week, introducing formal methods in general, and the technical and theoretical concepts behind the presented methods and tools. Some lectures contain hands-on exercises. The students perform practical case studies using the tools in lab assignments. There is one exercise class per week.

Litteratur

For the model checking part of the course, we recommend the book: M. Ben-Ari: Principles of the SPIN Model Checker. Springer. For the deductive verification part of the course, we recommend selected chapters of the book: B. Beckert, R. Hähnle, P. Schmitt (eds.): Verification of Object-Oriented Software - the KeY Approach. Springer. Lecture Notes in Computer Science, Vol. 4334, 2006 (available online via the Chalmers library).

Examination

There are two labs that can be done in groups of two. At the end of the course a written exam takes place. To pass the whole course it is necessary to pass both exam and labs, but they can be passed independently. The grade is determined by the result in the exam.


Sidansvarig Publicerad: on 24 jan 2018.