| Code |
14498
|
| Year |
1
|
| Semester |
S1
|
| ECTS Credits |
6
|
| Workload |
OT(15H)
|
| Scientific area |
Informatics
|
|
Entry requirements |
N/A --
|
|
Mode of delivery |
face-to-face
|
|
Learning outcomes |
This course addresses the concepts, the methodologies and tools that allow for the design of reliable (mathematically sound) applications, on an industrial scale.
Upon completion of the course, the students should be able to:
- study the different aspects of reliability
- Choose the appropriate technology, formalism and tools for a specific realiable software project.
- Modeling, implementing reliable systems
- Certify, that is prove with the help of the computer reliability results.
|
|
Syllabus |
From a theoretical point of view, this course introduces the mathematical models upon which it is possible to compute and reason about programs.
In its practical component, the course introduces how to design and use models of programs, how to test and verify correctness properties, before proceeding to the implementation stage and in order to avoid errors or bugs. In short: model, calculate, verify, test and evaluate.
|
|
Main Bibliography |
José Carlos Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification. Series: Undergraduate Topics in Computer Science, Springer. 1st Edition., 2011, XIII, 307 p. 52 illus. ISBN: 978-0-85729-017-5.
Development An Introduction to Program Verification. Springer Verlag, 2010.
Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer Verlag, 2004.
J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.
|
|
Teaching Methodologies and Assessment Criteria |
as a course included in a PhD program, the teaching is of a theoretical nature where the research questions are introduced and contextualised, where the most relevant results are also introduced and motivated.
The students will be required to read and master the relevant literature, to be acquainted with research tools that come from the state of the art. The assessment will look for measuring these familiarity with the subject and the acquired maturity in the use of the concepts but also the research tools.
|
|
Language |
Portuguese. Tutorial support is available in English.
|