MODELING AND VERIFICATION OF SOFTWARE SYSTEMS
MODELLAZIONE E VERIFICA DI SISTEMI SOFTWARE
|Lecturer||Office hours for students|
|Alessandro Aldini||Wednesday, from 10:00 am to 01:00 am|
Assigned to the Degree Course
The objective of this course is to introduce techniques for modeling the architecture of complex software systems and verifying their properties by means of formal methods based on languages, automata, logics, and algebra.
01. Introduction to modeling and verification:
01.01 The need for formal methods in software development.
01.02 Formal languages and automata.
01.03 Grammars and Chomsky classification.
01.04 Formal approaches to language semantics.
01.05 Concurrency theory, logics, and algebra.
02. Regular languages and finite-state automata:
02.01 Deterministic finite-state automata.
02.02 Nondeterministic finite-state automata.
02.03 Nondeterministic finite-state automata with epsilon-transitions.
02.04 Minimization and equivalence for finite-state automata.
02.05 Finite-state automata and linear grammars.
02.06 Closure properties of regular languages and pumping lemma.
02.07 Regular expressions.
02.08 Regular expressions and finite-state automata.
03. Context-free languages and pushdown automata:
03.01 Free grammars and syntax trees.
03.02 Chomsky normal form.
03.03 Properties of context-free languages.
03.04 Pushdown automata and relation with free grammars.
03.05 Top-down parsing.
03.06 Bottom-up parsing.
04. Denotational semantics:
04.01 Denotational semantics for an imperative language.
04.02 Denotational semantics for an imperative language with blocks and procedures.
05. Operational semantics:
05.01 Natural semantics for an imperative language.
05.02 Natural semantics for an imperative language with blocks and procedures.
05.03 Structural operational semantics for an imperative language.
06. Temporal logics and model checking:
06.01 Kripke models.
06.02 Temporal logics.
06.03 Linear-time logics vs. branching-time logics.
06.04 Model checking algorithms.
07. Process algebra and behavioral equivalences:
07.01 Concurrency and nondeterminism.
07.02 Syntax and semantics of behavioral operators.
07.03 Trace based equivalence.
07.04 Bisimulation based equivalence.
07.05 Test based equivalence.
08. Languages for the specification of software architectures:
08.01 Components, connectors, and architectural styles.
08.02 Syntax of an architectural language based on process algebra.
08.03 Semantics of an architectural language based on process algebra.
08.04 Behavioral conformity.
08.05 Topological extensions.
09. Laboratory activity:
09.01 Specification of software systems through Kripke models.
09.02 Specification of software systems through architectural languages.
09.03 Practice on model checking.
09.04 Practice on equivalence checking.
Discrete Structures and Linear Algebra, Procedural and Logic Programming.
Didactics, Attendance, Course Books and Assessment
Theory lectures and laboratory exercises, both face-to-face and on-line.
Although recommended, course attendance is not mandatory.
- Course books
Hopcroft, Motwani, Ullman, "Automi, Linguaggi e Calcolabilità", Addison-Wesley, 2009
Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, 2007).
Nielson, Nielson, "Semantics with Applications: An Appetizer", Springer, 2007
Clarke, Grumberg, Peled, "Model Checking", MIT Press, 1999
Aldini, Bernardo, Corradini, "A Process Algebraic Approach to Software Architecture Design", Springer, 2010
Individual project and written exam.
The written exam is associated with one and only one individual project, which is published 10 days before the written exam.
The project must be delivered by the written exam and is evaluated at most 10 points after an oral examination.
The written exam is evaluated at most 20 points.
The final mark is determined by the sum of the marks of written exam and individual project.
The course is offered both face-to-face and on-line within the Laurea Degree Program in Applied Computer Science.
|« back||Last update: 11/12/12|