Personen | Personen nieuwe site | Google | Route | Contact Login 
Course details 2012-2013  
    
Specification and verification
Course Code :2001WETFSP
Study domain:Computer Science
Semester:Semester: 1st semester
Contact hours:45
Credits:6
Study load (hours):168
Contract restrictions: No contract restriction
Language of instruction :English
Exam period:exam in the 1st semester
Lecturer(s)Dirk Janssens

 


1. Prerequisites

At the start of this course the student should have acquired the following competences:
Specific prerequisites for this course:
You have successfully completed a number of more complex programming projects and you have a basic knowledge of software engineering concepts.


2. Learning outcomes

Starting from an informal specification in natural language you have to write a specification in each of the formalisms considered. This specification should use in a sensible way the facilities offered by the languages: abstraction, refinement, modularity. You are also expected to be able to comment on a given specification, and you have to be able to explain the main characteristics of the various specification languages, their intended application area, etc.


3. Course contents

An important issue in the development of large software systems is the specification of its desired structural and dynamic properties. To avoid the impreciseness and ambiguities of specifications in natural language, a number of specialized formal languages, based on mathematics, have been developed: Hoare logic, Z, Alloy, etc. Moreover, these languages are supported by tools allowing various types of analysis and verification. The SPIN system is a prominent example of that. The course introduces the students to a number of specification and verification languages, their basic assumptions, tool support, advantages and limitations.


4. Teaching method

Class contact teaching:
  • Lectures
  • Practice sessions
  • Seminars

  • Personal work:
  • Casussen: Individually
  • Casussen: In group



  • 5. Assessment method and criteria

    Examination:
  • Oral with written preparation
  • Practical examination

  • Continuous assessment:
  • Assignments


  • 6. Study material

    Required reading

    For each of the specification languages discussed a number of papers and/or books will be made available.

    Optional reading

    The following study material can be studied on a voluntary basis:
    For the part on program logic: an extensive treatment can be found in:
     
    Krysztof R. Apt and Ernst-Rüdiger Olderog, Verification of Sequential and Concurrent Programs, Springer, ISBN 0-387-94896-1



    7. Contact information
    lecturer: Dirk.Janssens@ua.ac.be 
    (+)last update: 03/10/2012 10:55 dirk.janssens