School Courses
1 - Introduction and Motivations
Formal Methods for Computer System Design and Analysis - A Gentle Introduction Duration: 4 hours Day: September 6, afternoon Lecturer:
AbstractClick to Show/Hide Abstract
The tutorial starts with a discussion on the role of mathematically based notations and methods in the engineering tradition, e.g. electrical engineering. Emphasis will be put on the structural definition of such notations, where basic components and composition methods can be identified and are often provided with graphical representations. On the other hand, rigorous mathematical descriptions support such specification and modeling notations as well as reasoning about requirements and models, often with the help of automated, computer-based tools. Then, the discussion moves to Software/System Engineering and Formal Methods for System Engineering are motivated and introduced, with focus on concurrent systems and on an approach based on Process Algebra/Labelled Transition Systems and Temporal Logics. The issue of modeling system functional behaviour is recalled and State-Transition structures are introduced, as well as variants thereof, e.g. Labelled Transition Systems. The notion of process algebra is also introduced and its relationship with Labelled Transition Systems is briefly described; for concrete examples, a CSP-like language is used. The need and existence of notions of process equivalence(s), e.g. Bisimulation Equivalence is also addressed. The issue of system functional requirements specification is recalled and Temporal Logics are presented as a means for tackling, it in the context of Software/System Engineering. Computation Tree Structures are introduced as a means for representing system runs and their relationship with Labelled Transition Systems is addressed. Several examples of formalisation of system properties are shown, using a CTL-like logic. The use of Model-checking as an automated technique for checking system models against system requirement specifications is addressed, with reference to several success stories. Finally, probabilistic/stochastic extensions of modeling structures and languages as well as requirements specification logics are discussed. These allow to cover some aspects of non-functional features of systems, e.g. performance. The notions of Stochastic Process Algebra, Continuous Time Markov Chains, Stochastic Logics and Stochastic Model-Checking, as well as their relationships, are briefly introduced and some examples are given using the Performance Evaluation Process Algebra (PEPA) and the Continuous Stochastic Logic (CSL). The style of the tutorial is informal; concepts are introduced by means of simple examples, while formal definitions are avoided or reduced to the very minimum. No theorems, proofs or algorithms are presented, with the aim of making the tutorial accessible to an as wide audience as possible, maybe at the cost of some incompleteness, but still guaranteeing a good level of rigour. No background or basic knowledge on Formal Methods is assumed or required. The tutorial is composed of two lectures of two hours each. The first lecture covers introduction and motivations, Process Algebras, and Transition Systems. The second lecture covers Temporal Logics and stochastic extensions.
2 - Applications in orchestration of web services
Duration: 6 hours Day: September 7 Lecturers:
AbstractClick to Show/Hide Abstract
Specifying and analisying SOC applications with COWS The lecture starts with a brief introduction to Service-Oriented Computing (SOC). It will be explained the key notion of "service" and the use of services as the basic blocks for building interoperable and evolvable applications according to the SOC paradigm. Then, we will argue on the need of providing current software engineering technologies for SOC with rigorous formal foundations, which motivates the work described in the rest of the lecture. The role of process calculi will be explained by drawing a parallel between their algebraic nature and the compositional programming style of SOC. The lecture moves then to illustrate this approach by focussing on COWS (Calculus for Orchestration of Web Services), a process calculus for specifying and combining service-oriented systems whose design has been influenced by WS-BPEL, the OASIS standard language for orchestration of web services. COWS combines in an original way a number of ingredients borrowed from well-known process calculi, e.g. asynchronous communication, polyadic synchronization, pattern-matching, protection, delimited receiving and killing activities, while resulting different from any of them. COWS has proved to be sufficiently expressive both for modelling orchestration constructs, e.g. fault and compensation handlers, and all the phases of the life cycle of service-oriented applications, such as publication, discovery, negotiation, orchestration, deployment, reconfiguration and execution. The operational semantics of the calculus will be described together with many examples demonstrating COWS features and expressive power. Then, a number of methods and tools for analysing COWS terms will be introduced: among them, a type system to check confidentiality properties, and the temporal logic SocL and the model checker CMC (available at http://fmt.isti.cnr.it/cmc) to express and check functional properties of services. Afterwards, we will present Venus, a software tool (available at http://rap.dsi.unifi.it/cows) that facilitates access to the above model checking functionalities to users not familiar with process calculi and temporal logics. Stochastic COWS and its applications We will present sCOWS, an extension of COWS that semantically embeds stochasticity and hence allows modelling services whose behaviour can be analysed using Markovian techniques. For instance, Markov chains corresponding to sCOWS terms can be model checked against CSL (Continuous Stochastic Logic) formulas. As an example, we will detail how probabilistic model checking can be performed over sCOWS by applying a tool, named sCOWS_LTS and available at http://disi.unitn.it/~cappello/index.php?vis=dl. sCOWS_LTS generates the Labelled Transition System corresponding to the specification, and its subsequent translation to a Continuous Time Markov Chain that can be used as input for the PRISM probabilistic model checker. This will also involve a brief presentation of PRISM (available from http://www.prismmodelchecker.org/).
3 - Applications in systems biology
Duration: 6 hours Day: September 8 Lecturers:
AbstractClick to Show/Hide Abstract
We will present some approaches to the formal modeling of biological systems and to the verification of properties of such systems. Biological systems of interest include intra- and inter-cellular processes such as gene regulation mechanisms, metabolic pathways, signaling pathways, cell growth, tumor development, tissue development, etc... Initially, an introduction to the necessary notions of biology will be given with motivations for the application of formal modeling and analysis techniques in this field. Subsequently, some formal modeling approaches will be discussed, including the use of the Calculus of Looping Sequence, a recently proposed formalism for the description of cellular processes. These approaches allow biological systems to be described unambiguously and analysis tools to be developed, by taking also into account also quantitative aspects of the described systems. The complexity of biological systems and the often incomplete knowledge of the parameters often make it difficult to apply formal verification techniques such as model checking. We will present some abstraction and model reduction techniques that can be exploited to enable the application of probabilistic model checking to biological systems.
4 - Applications to safety-critical systems
Duration: 3 hours Day: September 9, Morning Lecturer:
AbstractClick to Show/Hide Abstract
Due to the possibility offered by model checking to give a definite result on the satisfaction of a property by a system, model checking has been considered as a very interesting technique in the realm of critical systems, where safety could be put at stake by software errors. However, modern safety critical systems are very complex, and application of model checking of such large systems has to face important scalability problems. Moreover, relations with guidelines and norms for safety critical systems have to be taken into account; another important issue from the industrial point of view is the availability of commercial or industrial strength tool, and their own reliability. We discuss these issues also presenting some applications of model-checking in real word safety critical systems, from the application domains of avionics and railway signalling.
5 - Applications in human-computer interaction
Duration: 6 hours Day: September 9 - 10 Lecturers:
AbstractClick to Show/Hide Abstract
Qualitative and Quantitative Formal Analysis in HCI The course, after a brief introduction to the foundations of Human-computer Interaction, is structured in two parts: a first part on qualitative analysis and a second part on quantitative analysis. The first part of the course starts by illustrating the challenge of taking human errors into account while modelling interactive systems and by investigating the nature and aspects of human error with reference to practical examples. It then presents how to incorporate human behaviour in the modelling of interactive systems and how to apply model-checking methodologies to the formal analysis of qualitative aspects of such systems. This part of the course will focus on important cognitive aspects of human behaviour, such has the role of short-term memory in goal-based tasks and the switching between automaticity and attention, as well as the emergence of cognitive errors and their detection using model-checking. In the second part of the course quantitative aspects of human cognition and human factors will be taken into account in models of interactive systems. In particular the modelling of these aspects will be illustrated by means of a case study on human interruptions. In many modern working environments interruptions are commonplace as users must temporarily suspend a task to complete an unexpected intervening activity. As users are faced with more and more sources of information competing for their attention, it is becoming increasingly important to understand how interruptions affect their abilities to complete tasks. This part of the course introduces a new perspective for research in this field by employing model-based techniques that are informed by well-established cognitive theories that illustrate how humans deal with multiple sources of information. Also empirical data on human factors, available in the literature, are taken into account. Stochastic modelling and model checking will be introduced to predict measures of the disruptive effects of interruptions to two interaction techniques: Drag 'n Drop and Speak 'n Drop. The approach also provides a way to compare the resilience of different interaction techniques to the presence of external interruptions that users need to handle. The obtained results are in a form that allows validation with results obtained by empirical studies involving real users.
6 - Applications in security of systems
Policies for Safe Service Composition Duration: 3 hours Day: September 10, afternoon Lecturers:
AbstractClick to Show/Hide Abstract
We propose a framework (named "lambda-req") for reasoning about the safe composition of services. We start by defining a suitable programming model for services; then, we study how to use policies to specify requirements on the run-time behaviour. Finally, we consider how to statically verify that a service complies with a given set of policies. The first part of the discussion will introduce the programming model. Lambda-req is a minimal, "core" language which extends the call-by-value lambda-calculus with side effects and service invocation. Its operational semantics collects all the side effects in a history, hence providing execution traces. Then, we shall use (a variant of) finite state automata to define policies, which are used to constrain executions. Policies can be applied to constrain the whole system ("global policies"), or just one portion of it ("local policies"). Further, policies can also be used to drive the service invocation mechanism. This provides the so-called "call-by-contract" service invocation. Run-time enforcement of policies is feasible, at the cost of performing run-time checks. Alternatively, we can statically verify policies: when this succeeds, we can safely skip run-time checks. Static verification is done in several steps. First, we use a type and effect system to 1) check that a given lambda-req specification is type-safe (in the usual sense, e.g. "do not sum strings"), and 2) extract from the code a sound over-approximation of all the possible run-time histories. This over-approximation is represented as a History Expression, which is a term in a simple recursive language. History Expressions are then manipulated and simplified through several transformations, and finally reduced to Basic Process Algebras (BPA). Finally, BPA can then be compared against policies: if no violation arises, the original lambda-req specification is guaranteed to be safe. The framework is presented in two lectures. The first lecture (1h) will cover the programming model, the policies, and the basics underlying the type system. The second one (2h) will introduce the type system, the transformation of history expressions, as well as the rest of the verification machinery. |
www.sefm2010.isti.cnr.it SEFM 2010 School | |
Home | News | Downloads | | rss feed | css 2.1 | last updated: 04 Oct, 2010 - 08:08 |