Università degli Studi di Urbino Carlo Bo / Portale Web di Ateneo


MODELING AND VERIFICATION OF SOFTWARE SYSTEMS
MODELLAZIONE E VERIFICA DI SISTEMI SOFTWARE

Modeling and Verification of Software Systems
Modellazione e Verifica di Sistemi Software

A.Y. Credits
2014/2015 12
Lecturer Email Office hours for students
Alessandro Aldini Wednesday, from 10:00 am to 01:00 am

Assigned to the Degree Course

Date Time Classroom / Location

Learning Objectives

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.

Program

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.

Bridging Courses

Although there are no mandatory prerequisites for this exam, students are strongly recommended to take it after Procedural and Logic Programming, Computer Architecture, Discrete Structures and Linear Algebra.

Teaching, Attendance, Course Books and Assessment

Teaching

Theory lectures and laboratory exercises, both face-to-face and on-line.

Attendance

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

Assessment

Individual project, written exam, and oral exam. The individual project must be submitted at least two days before the written exam and its mark is at most 10/30. The mark of the written exam is at most 20/30. The oral exam is mandatory about the individual project and is optional about the course program. The optional oral exam yields a positive or negative adjustment to the final mark.

Disability and Specific Learning Disorders (SLD)

Students who have registered their disability certification or SLD certification with the Inclusion and Right to Study Office can request to use conceptual maps (for keywords) during exams.

To this end, it is necessary to send the maps, two weeks before the exam date, to the course instructor, who will verify their compliance with the university guidelines and may request modifications.

Notes

The course is offered both face-to-face and on-line within the Laurea Degree Program in Applied Computer Science. For additional lecture notes and information see http://www.sti.uniurb.it/aldini/

« back Last update: 23/10/2013

Il tuo feedback è importante

Raccontaci la tua esperienza e aiutaci a migliorare questa pagina.

Il tuo 5x1000 per sostenere le attività di ricerca

L'Università di Urbino destina tutte le risorse che deriveranno da questa iniziativa alla ricerca scientifica ed al sostegno di giovani ricercatori.

15 22

Se sei vittima di violenza o stalking chiama il 1522, scarica l'app o chatta su www.1522.eu

Il numero, gratuito è attivo 24 h su 24, accoglie con operatrici specializzate le richieste di aiuto e sostegno delle vittime di violenza e stalking.

Posta elettronica certificata

amministrazione@uniurb.legalmail.it

Social

Università degli Studi di Urbino Carlo Bo
Via Aurelio Saffi, 2 – 61029 Urbino PU – IT
Partita IVA 00448830414 – Codice Fiscale 82002850418
2024 © Tutti i diritti sono riservati

Top