Formal Methods in Software Engineering
Keywords |
Classification |
Keyword |
OFICIAL |
Software Engineering |
Instance: 2009/2010 - 2S
Cycles of Study/Courses
Teaching language
Portuguese
Objectives
1- BACKGROUND
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
Scientific component:50%
Technological component:50%
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.
Program
1. Introduction
What are formal methods?
Importance and applicability of formal methods in the development of software
Life cycle models and software development processes by incorporating formal methods.
Specification, refinement, implementation, verification and validation
Classification of formal methods
Explicit vs. implicit models, executable vs. non-executable
Formal verification techniques
2. Alloy Constraint Analyser for modelling and semantic analysis
Declarative modelling
Difference related to model checking
Alloy commands
Functions; predicates; facts; assertions and verifications (checks)
Static vs. dynamic modelling
Simulation of an operation
Check safety properties
Alloy analyser tool
3. Logic and model checking
Propositional, predicate, linear temporal (LTL) and computer tree logic (CTL)
State representation
Model checking:
- properties: safety, fairness, liveness, universality, possibility, absence, response, precedence
- The state explosion problem (techniques to diminish the problem): Symbolic state; bounds; on-the-fly; Partial Order Reduction (POR); abstraction
4. Model Based Specification
VDM-SL and VDM++ languages
Data representation based on mathematical structures (sets, sequences, finite functions)
State and non-state specification
Definition of types, values and functions
Definition of classes, instance variables and operations
Expressions and instructions
Design-by-contact: definition of invariables, preconditions and postconditions
Description of algorithms, executable specifications
Analysis of specification consistency
Connection of VDM++ to UML
Code generation from a formal specification
VDMTools
5. Formal proofs
Application of Hoare’s logic to algorithm correction
Gallina specification language: types of expressions, propositions and proofs; inductive data types; proof and automation tactics; inductive predicates
Program Correctness Proof
Coq, Caduceus, JAPE and Krakatoa
Mandatory literature
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
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
Complementary Bibliography
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.
Software
VDMTools
Coq
Krakatoa
JAPE
Alloy Analyzer
Caduceus
keywords
Technological sciences > Engineering > Computer engineering
Technological sciences > Technology > Computer technology > Software technology
Evaluation Type
Distributed evaluation with final exam
Assessment Components
Description |
Type |
Time (hours) |
Weight (%) |
End date |
Attendance (estimated) |
Participação presencial |
64,00 |
|
|
|
Exame |
12,00 |
|
2010-07-31 |
|
Defesa pública de dissertação, de relatório de projeto ou estágio, ou de tese |
50,00 |
|
2010-06-26 |
|
Total: |
- |
0,00 |
|
Amount of time allocated to each course unit
Description |
Type |
Time (hours) |
End date |
|
Estudo autónomo |
36 |
2010-07-24 |
|
Total: |
36,00 |
|
Eligibility for exams
Students have to reach a minimum mark of 45% in the continuous assessment component.
Students have to reach a minimum mark of 45% in the exame.
Calculation formula of final grade
Final Mark will be based on the following components:
a) Open book exam – 2h 30m (50% of the final mark) – minimum mark of 45% (E)
b) Continuous assessment (50% of the final mark)
- Practical assignment, which is worth 25%- minimum mark of 45% (P1)
- Practical assignment, which is worth 25%- minimum mark of 45% (P2)
Final grade = E*50% + P1*25% + P2*25%
Comment: The difference between Final Mark and the mark of the exam cannot be higher than 2.5 values. It will be adjusted if it is.
Examinations or Special Assignments
The assignments are mandatory to all students, even the ones who do not need to attend classes.
Classification improvement
Students can improve the mark of their exams by attending a new exam at recurso season.
Students can only improve the mark of the continuous assessment component in the following year.