• Understanding generic techniques for analysis of software source code. • Implement tools for the anlysis of software programs and systems. • Understanding the concepts of software quality and modles of software quality. • Develop automatic tools for software quality analysis based on software metrics. • Implement software tools for the transformation, refactoring and evolution of programs. • Implement essential algorithms for the static analysis of programs.
The course on Software Analysis and Testing consists of the following four topics: • Source Code Analisys: Scannerless and Generalised Parsing techniques, Parser Combinators, Generic Tree Traversals, Strategic Programming, Type Analysis, Data Flow Analysis, Inter-procedural Analysis, and flow control analysis. • Software Quality: Source code metrics, software system metrics, empirical studies for software quality assessment, software quality models (CMMI, ISO 9126), software certification. • Transformation of Software: Techniques for source code transformation and refactoring (use of the software systems TOM and RASCAL), Slicing and partial evaluation, Software Evolution, Model-driven software development and evolution. • Software Testing: Unit and functional testing; analysis of test coverage; model based testing; automatic generation of test cases; fault localization and fault injection. Testing in JUnit + Emma, QuickCheck and PEX systems.
This curricular unit is structured in two parts: one theoretical part where the theory and techniques involved in each of the four areas of the Syllabus are introduced and studied; A second part consisting of a small project developed by the students throughout the course, so that they have the opportunity to use tools that implement the concepts introduced in the theoretical part. The evaluation considers these two parts of the course and they have the same weight in the evaluation: in the theoretical part of the course the student will have a written, individual exam, and in the practical part the students will developed a software group project.
• Generative and Transformation Techniques in Software Engineering I, II, III, Ralf Laemmel, Joost Visser and João Saraiva editors, volumes 4143 and 5235 of LNCS Tutorials, proceedings of the summer schools GTTSE’05, GTTSE’07 and GTTSE’09, Springer. • Generative Programming - Methods, Tools, and Applications, Krzysztof Czarnecki and UlrichW. Eisenecker, Addison-Wesley, June 2000. • Partial Evaluation and Automatic Program Generation, N.D. Jones, C.K. Gomard, and P. Sestoft, Prentice Hall International, June 1993 • Domain Specific Languages, Martin Fowler, Addison-Wesley Professional, September, 2010 • Refactoring: Improving the Design of Existing Code, Martin Fowler, Kent Beck, John Brant,William Opdyke, Don Roberts, Addison Wesley, 2000. • Software Evolution, Tom Mens, Serge Demeyer, Springer 2008. • Software Testing, Ron Patton, Sams Publication 2006
To abstract the details of a software component in order to obtain a model suitable for formal verification; To model the state of a software component using the unifying concept of mathematical relation; To specify invariants and pre- and post-conditions of operations using relational logic; To specify reactive systems using temporal logic; To use automatic verification tools to establish the validity of a given software property.
Introduction: the role of formal methods in software engineering; the role of abstraction in formal modeling; propositional and first-order logic. Relational logic: syntax and semantics; modeling using relations; introduction to the relational calculus; taxonomy and relational algebra. Alloy: speficiation of invariants and operations using pre- and post-conditions using relational logic; idioms for modeling dynamic behaviour; semantics and type system; automatic verification techniques; comparison with other modeling languages. Specification of reactive systems: temporal logic (LTL and CTL); explicit state model checking; symbolic model checking; tools for model checking.
Teaching methodology: theoretic lectures; practical lectures with tool demonstrations and exercise solving; Evaluation: Alloy mini-project (10%); Model checking mini-project (10%); Reading assignment (10%); individual exam (70%). The mini-projects and reading assignment are developed in groups of 2 students.
Daniel Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
This course, which integrated the profile in Formal methods in Software Engineering, introduces Software Architecture from a formal perspective and entirely focussed on reactive systems. It aims at a. characterising transition systems as a basic architectural design structure for reactive systems b. introducing suitable mathematical foundations: relational calculus and linear algebra of programming c. addressing in detail two paradigms in architectural design: process and coordination-oriented design d. introducing techniques for architectural analysis at structural, behavioural and performance levels At the end of the course, students will a. be familiar with basic formal structures for architectural design of reactive systems b. be able to model software architectures in suitable formal frameworks c. exhibit practical skills in analysing reactive software architectures for functional correctness, structural organisation and performance.
1. Introduction to software architecture and reactive systems: problems,concepts and methods. 2. Foundations: 2.1 Transition systems as a basic architectural design structure. Simulation, bisimulation and invariants. Relational calculus and Galois connections. Relationship with modal logic and process algebra. 2.2 Weighted automata and stochastic behaviour. Introduction to the linear algebra of programming. 3. Paradigms of architectural design 3.1 Process-oriented design. Introduction to AADL. 3.2 Coordination-oriented design. Introduction to Reo. 4. Architectural analysis 4.1 Structural, behavioural and performance properties. 4.2 Interactive Markov chains for architectural analysis. Laboratory: Development of medium size case studies in architectural design and analysis, resorting to a number of computer-supported tools for AADL, Reo and Markov chains.
Teaching methodologies combine classical lectures, exercise classes and laboratory sessions. The latter aims at trainning students in the correct use of tools. Asessment is carried on through an individual written test (60%) and the development of a number of mini- projects with the tools introduced along the course (40%).
A. Aldini, M. Bernardo, and F. Corradini. A Process Algebraic Approach to Software Architecture. Springer Verlag, 2010. F. Arbab. Reo: a channel–based coordination model for component composition. Mathematical Structures in Comp. Sci., 14(3):329–366, 2004. D. Garlan. Formal modeling and analysis of software architecture: Components, connectors and events. In M. Bernardo and P. Inverardi, editors, Third International Summer School on Formal Methods for the Design of Computer, Communication and Software Systems: Software Architectures (SFM 2003). Springer Lect. Notes Comp. Sci, Tutorial, 2004. Holger Hermanns. Interactive Markov Chains. Springer Verlag. 2002. J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.), volume 23 of CRM Monograph Series. American Mathematical Society, 2004.
• To explain the the principles underlying the most important techniques in program verification. • To specify the behaviour of programs through the use of contracts. • To use tools for the deductive verification of programs annotated with contracts. • To explain the different approaches that have been used to mitigate the state space explosion problem in model checking. • To use a symbolic model checking tool. • To apply automatic software verification tools based on model checking.
• Theorem proving: introduction to the interactive construction of proofs. • First order theories: employing SMT solvers. • Deductive verification: program logics; verification condition generation; behavioral interface specification languages and design by contract. Tools covered: Dafny; Frama-C; SPARK. • Model Checking: symbolic model checking ; partial order reduction; bounded model checking. Tool covered: SMV. • Software Model Checking: bounded model checking of software; existential abstraction mechanisms; predicate abstraction; abstraction refinement. Tools covered: CBMC; BLAST.
The contact time in this UC is employed as follows: - Two weekly lectures present the theoretical concepts and case studies. - Complementarily, two weekly TP classes (tutorials) are used for solving exercises or presenting case studies (using the selected tools), as well as for other points, such as discussing and accompanying possible miniprojects to be developed by the students. Assessment is made through two tests (intermediate and final), both weighing 50%, or alternatively through one test (60%) and one verification miniproject (40%).
- Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York, NY, USA. - Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 2000. Model Checking. MIT Press, Cambridge, MA, USA. - José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, and Simão Melo de Sousa. 2011. Rigorous Software Development: An Introduction to Program Verification (1st ed.). Springer Publishing Company, Incorporated. - Aaron R. Bradley and Zohar Manna. 2010. The Calculus of Computation: Decision Procedures with Applications to Verification (1st ed.). Springer Publishing Company, Incorporated.