Courses

Day Morning Afternoon
23.11 OO CSP
24.11 OO CSP
25.11 OO CSP
26.11 Prob Tools
27.11 Prob Tools/Panel
28.11 Prob UTP
2.12 UTP UTP
3.12 RT MC
4.12 RT MC
5.12 RT MC

Morning and Afternoon Sessions

08:30 - 10:30 Morning Lecture (Part I)
10:30 - 11:00 Coffee Break
11:00 - 12:30 Morning Lecture (Parte II)
12:30 - 14:00 Lunch
14:00 - 16:00 Afternoon Lecture (Part I)
16:00 - 16:30 Coffee Break
16:30 - 18:00 Afternoon Lecture (Part II)

Important: on the first day (23rd November) the material should be collected between 8-8:30 at the room Mingos, where the sessions will take place

Legend

  • UTP
    Unifying Theories of Programming
    Ana Cavalcanti, Jim Woodcock

    The book by Hoare & He sets out a research programme to find a common basis in which to explain a wide variety of programming paradigms: unifying theories of programming (UTP). Their technique is to isolate important language features, and give them a denotational semantics. This allows different languages and paradigms to be compared. The semantic model is an alphabetised version of Tarski's relational calculus, presented in a predicative style that is reminiscent of the schema calculus in the Z notation. Each programming construct is formalised as a relation between an initial and an intermediate or final observation. In this course, we discuss the model of CSP processes.

    Suggestions for reading material:
    • C. A. R. Hoare and He Jifeng. Unifying Theories of Programming. Prentice-Hall, 1998
    • J. C. P. Woodcock and A. L. C. Cavalcanti. A Tutorial Introduction to Designs in Unifying Theories of Programming IFM 2004: Integrated Formal Methods, Invited tutorial. Pages 40-66, Springer-Verlag, Lecture Notes in Computer Science, Vol. 2999, 2004
  • CSP
    Concurrency: CSP + FDR
    Jim Davies

    This is a tutorial on Communicating Sequential Processes (CSP): a language for modelling patterns of behaviour. It explores the design of the language, and shows how it may be used to construct precise descriptions of dynamic properties and distributed systems. It explains how the use of the language may be supported by verification tools, and discusses how it can form part of a precise, object-based modelling framework. Exercises, and a short bibliography, are included.

    Suggestion for (accessible) reading material:

  • OO
    Refinement in object-oriented development: Sequential Java
    Paulo Borba, Augusto Sampaio

    The main objective of this tutorial is to explore the algebraic laws of object-oriented programming. We describe a comprehensive set of laws for a language that is similar to a subset of sequential Java.

    As initial background we present laws that deal with the imperative features of our language, and introduce the basic notions of algorithmic and data refinement. Then we concentrate on laws for object-oriented features. We show that our set of laws is complete in the sense that it is sufficient to reduce an arbitrary program to a normal form substantially close to an imperative program.

    Besides clarifying aspects of the semantics of object-oriented constructs, the major application of our laws is to formally derive more elaborate behaviour preserving program transformations useful for optimising or restructuring object-oriented applications. In particular, we show how they can be used to derive provably-correct refactorings.

    Suggestions for reading material:

    • Paulo Borba, Augusto Sampaio, Ana Cavalcanti, Marcio Cornélio. Algebraic Reasoning for Object-Oriented Programming. Science of Computer programming, (52):53-100, 2004.
    • Carroll Morgan. Programming from Specifications. Prentice Hall, 2nd edition, 1994. Available at http://users.comlab.ox.ac.uk/carroll.morgan/PfS/
  • Prob
    Probability in the context of wp
    Carroll Morgan

    The presentation explains and motivates a programming logic and semantics that includes both demonic and probabilistic nondeterminism. The former is used to control abstraction and refinement while developing algorithms and systems; the latter allows those systems to contain exhibit probabilistic .that is, quantifiably random. behaviour. Probability is important for random algorithms, for distributed systems and for quantification of risk and cost.

    The individual lectures will first cover elementary sequential programs (based on Dijkstra's minimally-syntaxed programming language GCL), loops and their associated invariant/variant reasoning tools, and the relational operational model whose existence validates the approach. Later lectures will explore more exotic topics such as probabilistic temporal logic and µ-calculus, and their connection to angelic/demonic/probabilistic games.

    Suggestions for reading material at:
  • RT
    Real-Time and Fault-Tolerant Systems: Specification, Verification, Refinement and Schedulability
    Zhiming Liu

    Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs.

    This course discusses how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be used to combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using a simple example.

    Suggestions for reading material:
    • Liu Z. and Joseph M. (1999) Specification and verification of fault-tolerance, timing and scheduling , ACM Transactions on Languages and Systems, Vol. 21, No. 1, January (1999), pp. 46-89.
    • Mathai Joseph (Editor) (1996) Real-time Systems: Specification, Verification and Analysis, Prentice Hall (1996). Available at http://www.tcs.com/techbytes/htdocs/book_mj.htm
  • Tools
    Refinement tools: focus on industrial experience
    Philip Clayton

    Evidence has shown that safety failures arise not so much as a result of programming errors but as a result of higher-level design decisions or incorrect identification of requirements. A contributing factor is the lack of accurate and precise documentation and the ability to maintain such documentation. The most accurate record of all implementation decisions is the source code itself however this is not amenable to human understanding thus a means of abstracting the source code is needed. This tutorial introduces a notation that enables compliance to be shown between specification and code, either as code is developed or retrospectively, and a tool that supports reasoning with this notation. We show how this tool is used to check safetly properties, how it is built on to verify programs that implement Simulink block diagrams and, finally, how it is used as part of a wider safety argument for a software system.

    Suggestions for reading material:
    • Ch. 1 - 7, Programming from Specifications, Carroll Morgan, Prentice-Hall International series in computer science, 1990. Available at http://users.comlab.ox.ac.uk/carroll.morgan/PfS/
    • Ch 1 - 3, 11, 12, Using Z, Jim Woodcock & Jim Davies, Prentice-Hall International series in computer science, 1996
  • MC
    Model Checking
    David Deharbe

    The term "model checking" has been used to qualify a large variety of different automated formal verification techniques that aim to show that a (model of a) system satisfies (partial) correctness properties. In this course, we will mainly address two so-called "classic" model checking techniques: symbolic model checking and automata-based model checking. The presentation of these techniques will be supported by hands-on experiments with two of the most well-known implementations of model checking: NuSMV and SPIN. We will also briefly overview "modern" model checking, a complex combination of advanced methods that has been successful for the verification of software at the source level.

    Suggestions for reading material:
    • David Déharbe. Logic for Concurrency and Synchronisation, volume 18 of Trends in logic, chapter A tutorial introduction to model checking, pages 215-238. Kluwer Academic Publisher, 2003. Edited by Ruy J.G.B. de Queiroz. ISBN 1-4020-1270-5. [ .ps ]
    • Gerard Holzmann. The Model Checker Spin, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295. [ .pdf ]



Sponsors

 

 

 

 

[ Pernambuco School on Software Engineering: Refinement | Recife.PE ]