Formal Methods in Software Engineering
Instance: 2012/2013 - 1S
Cycles of Study/Courses
Teaching - Hours
Suitable for English-speaking students
Students should have knowledge about software processes and software modelling.
2- SPECIFIC AIMS
To develop abstraction capabilities in order to describe what the system should do and not the way to do it. Be familiar with formal methods and the way they can contribute to increase the quality of software systems.
3- PREVIOUS KNOWLEDGE
Software engineering; Computing Theory; Algorithm design and analysis.
4- PERCENT DISTRIBUTION
5- LEARNING OUTCOMES
At the end of the course students should be able to:
- Apply formal methods of specification (based on models, based on properties, based on behavior) and verification ("Model-checking, formal proofs and test) in the development of software systems.
- Identify existing formal methods and know when they should be applied and which are most suitable in each case.
1.1 What are formal methods?
1.2 Importance and applicability of formal methods in the development of software
1.3 Life cycle models and software development processes by incorporating formal methods.
1.4 Specification, refinement, implementation, verification and validation
1.5 Classification of formal methods
1.6 Explicit vs. implicit models, executable vs. non-executable
1.7 Formal verification techniques
2. Alloy Constraint Analyser for modelling and semantic analysis
2.1 Declarative modelling
2.2 Difference related to model checking
2.3 Alloy commands
2.4 Functions; predicates; facts; assertions and verifications (checks)
2.5 Static vs. dynamic modelling
2.6 Simulation of an operation
2.7 Check safety properties
2.8 Alloy analyser tool
3. Model Based Specification
3.1 VDM-SL and VDM++ languages
3.2 Data representation based on mathematical structures (sets, sequences, finite functions)
3.3 State and non-state specification
3.4 Definition of types, values and functions
3.5 Definition of classes, instance variables and operations
3.6 Expressions and instructions
3.7 Design-by-contact: definition of invariables, preconditions and postconditions
3.8 Description of algorithms, executable specifications
3.9 Analysis of specification consistency
3.10 Connection of VDM++ to UML
3.11 Code generation from a formal specification
4. Model Based Specification (OCL)
4.1 OCL language
4.2 Comparison with VDM++.
5. Logic and model checking
5.1 Propositional, predicate, linear temporal (LTL) and computer tree logic (CTL)
5.2 State representation
5.3 Model checking:
5.3.1 properties: safety, fairness, liveness, universality, possibility, absence, response, precedence
5.3.2 The state explosion problem (techniques to diminish the problem): Symbolic state; bounds; on-the-fly; Partial Order Reduction (POR); abstraction
6. Formal proofs
6.1 Application of Hoare’s logic to algorithm correction
6.2 Gallina specification language: types of expressions, propositions and proofs; inductive data types; proof and automation tactics; inductive predicates
6.3 Program Correctness Proof
6.4 Coq, Caduceus, JAPE and Krakatoa
Daniel Jackson; Software Abstractions, MIT Press, 2006. ISBN: 0-262-10114-9
Fitzgerald, John; Validated designs for object-oriented systems
. ISBN: 1-85233-881-4
Jos Warmer e Anneke Kleppe; The Object Constraint Language Second Edition
. ISBN: 978-0-321-17936-4
Richard Bornat; Proof and Disproof in Formal Logic, Oxford University Press, 2005. ISBN: 0-19-8530269
B. Bérard; M. Bidoit; A. Finkel; F. Laroussinie; A. Petit; L. Petrucci; Ph. Schnoebelen; P. McKenzie; Systems and Software Verification - Model Checking Techniques and Tools, Springer, 2001. ISBN: 3-540-41523-8
Clarke, Jr., Edmund M.; Model checking
. ISBN: 0-262-03270-8
Fitzgerald, John; Modelling systems
. ISBN: 0-521-62605-6
Alagar, V. S.; Specification of software systems
. ISBN: 0-387-98430-5
Teaching methods and learning activities
Theoretical classes will be based on the presentation of the themes of the course.
Practical classes will be based on exercises, so that students can contact with the various tools available and to do their assignments.
Octopus: OCL Tool for Precise Uml Specifications
Technological sciences > Technology > Computer technology > Software technology
Technological sciences > Engineering > Computer engineering
Distributed evaluation with final exam
|Mini and final exams
|Study for realization of practical work
Amount of time allocated to each course unit
Eligibility for exams
Students have to reach a minimum mark of 45% in the continuous assessment component.
The presence in the practical classes is recorded and mandatory according to existing legislation.
Calculation formula of final grade
Distributed evaluation with final exam, with the following components:
(A) Open book mini-test (Alloy) - 1 hour (40% of the final mark), minimum grade of 45%.
(B) Practical work - (25% of the final mark), minimum grade of 45%.
(C) Open book final exam - 1h 30m (35% of the final mark), minimum grade of 45%.
Final grade = (A) * 40% + (B) * 25% + (C) * 35%
Comment: The difference between Final Mark and the mark of the exam cannot be higher than 3 points. It will be adjusted if it is.
Students who fail to obtain approval in Alloy mini test module may make a further assessment on the final exam of the course.
The Alloy component can only be improved in second exame.
Examinations or Special Assignments
Mini Exam about Alloy on the 31st October.
Practical work of VDM++:
- Delivery by 23:00 on the 7th December;
- Defense of practical work during the practical lessons of the week 10 Dec -14 Dec.
The defense of practical work is mandatory for ALL students.
Special assessment (TE, DA, ...)
Students excused from attendance at practical classes should contact the teacher for special sessions of follow up.
The defense of practical work is mandatory for ALL students.
- The classification of the mini exam can only be improved in the appeal exam.
- Students who do not obtain approval in mini exam may make an additional module of 1h in the appeal exam.
- The marks obtained in practical work can be improved in the next edition of the discipline
- The classification of the test can be improved by in the appeal exame.
Students with class attendance in the previous year will have to take an exam with 2h30 (including the Alloy component).
The marks obtained in the previous year in the work of VDM++ will be used as a mark for the work in VDM++ of this edition.