Software Engineering using
Formal Methods
TDA293/DIT270, LP1, HT2015

About This Course

People

  • Wolfgang Ahrendt (examiner, lecturer)
  • Mauricio Chimento (course assistant)
  • Raúl Pardo (course assistant)
  • The course assistants Mauricio (room 5446, EDIT building) and Raúl (room 5447, EDIT building) offer scheduled office hours to help you with questions. You can make an appointment with one of them by email. It is not very likely that they are available if you just drop in.

    If you have any general questions regarding the course, please post in our google group. This will reach all teachers and your fellow students. This way, there can be an exchange of questions, hints, and discussions among all of us. Please make use of this forum. If you are not yet a member of the group, you have to

    • get a google account,
    • request an invitation to the sefm group, and
    • provide your personnumber and a valid Chalmers or Gothenburg University address (in the additional comment box) when applying for an invitation. This is necessary to identify you as a participant of the course.
    You can do all of that on the group page.

    All kinds of questions (and answers) on the content of the course are welcome. (But don't post lab solutions!)

    Examination

    To pass the course a student must

    Two courses in one

    The course is available both for Chalmers students and for GU students.

    Schedule

    The lectures and exercises are held in room EA. Please check Lectures and Schedule for directions.

    Course Content

    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 Gothenburg University, 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

    Familiarity with Java is encouraged.

    After successful completion of the course you will be able to:

    • judge the potential and limitations of using logic based verification methods for assessing and improving software correctness,
    • judge what can and what cannot be expressed by certain specification/modelling formalisms,
    • judge what can and cannot be analysed with certain logics and proof methods,
    • differentiate between syntax, semantics, and proof methods in connection with logic-based systems for verification
    • 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, using the concepts of method contracts and class invariants,
    • describe how the connection between programs and formal specifications can be represented in a program logic,
    • verify functional properties of simple Java programs with a verification tool,
    • acknowledge the socio-economical costs caused by faulty software,
    • judge and communicate the significance of correctness for software development,
    • approach the issue of correctly functioning software by means of abstraction, modeling, and rigorous reasoning

    Course Literature

    For the first part we use the book Principles of the Spin Model Checker, mostly Chapters 1-5. The book is available as E-book from the Chalmers network.

    For the second part, we do not have a proper course book. Still, there is highly relevant material in the book Verification of Object-Oriented Software: The KeY Approach (accessible from the Chalmers network). Chapter 1 in the book gives a general introduction in the philosophy behind KeY. In Chapter 10, written by the course teacher, is a tutorial on practical usage of the KeY prover. (Chapter 10 is however not fully up-to-date. We are currently writing a new version of the book and this chapter.)




    Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt , Aug 27, 2015