FACS 2011
8th International Symposium on Formal Aspects of Component Software

Oslo, Norway, September 14-16, 2011


José Meseguer (University of Illinois at Urbana-Champaign, USA)


Taming Distributed System Complexity through Formal Patterns

Abstract: Many current and future distributed systems are or will be:

  • real-time and cyber-physical
  • probabilistic in their operating environments and/or their algorithms
  • safety-critical, with strong qualitative and quantitative formal requirements
  • reflective and adaptive, to operate in changing and potentially hostile environments.

Their distributed features, their adaptation needs, and their real-time and probabilistic aspects make such systems quite complex and hard to design, build and verify, yet their safety-critical nature makes their verification essential. One important source of complexity, causing many unforeseen design errors, arises from ill-understood and hard-to-test interactions between their different distributed components.

Methods to tame and greatly reduce system complexity are badly needed. System complexity has many aspects, including the complexity and associated cost of:

  • designing
  • verifying
  • developing
  • maintaining and
  • evolving

such systems.

The main goal of this talk is to propose the use of formal patterns as a way of drastically reducing all the above system complexity aspects. By a "formal pattern" I mean a solution to a commonly occurring problem that is:

  • as generic as possible, with precise semantic requirements for its parameters
  • formally specified
  • executable, and
  • comes with strong formal guarantees.

This means that a formal pattern can be applied to a potentially infinite set of concrete instances, where each such instance is correct by construction and enjoys the formal guarantees ensured by meeting the semantic requirements of the pattern's parameters.

The overall vision is that distributed systems should be designed, verified, and built by composing formal patterns that are highly generic and reusable and come with strong formal guarantees. A large part of the verification effort is spent in an up-front, fully generic manner, and is then be amortized across a potentially infinite number of instances. As I will show through concrete examples, this can achieve very drastic reductions in all aspects of system complexity, including the formal verification aspect. It can lead to high-quality, highly reliable distributed systems at a fraction of the cost required not using such patterns.

To develop formal patterns for distributed systems with features such as those mentioned above an appropriate semantic framework is needed, one supporting:

  • concurrency
  • real time and probabilities
  • distributed reflection and adaptation, and
  • formal verification methods.

I will use rewriting logic as such a semantic framework, and will show in number of examples its adequacy to specify and verify formal patterns of this nature.

 

John Rushby (Computer Science Laboratory, SRI International, USA)


Composing Safe Systems

Abstract: We consider component-based systems that must ensure critical properties such as safety. We describe the value of partitioning, and of assumption synthesis, and suggest areas for further research.

 

Ketil Stølen (SINTEF ICT, Oslo, Norway)


Components and Risk

Abstract: Risk analysis is an important tool to establish the appropriate protection or safety level of a system. Unfortunately, the shifting environment of components is not adequately addressed by traditional risk analysis methods. Furthermore, the issue of risk is hardly addressed within methods for component-based system development. This talk will present challenges with respect to components and risk from three viewpoints, namely an industrial viewpoint, a modelling viewpoint and a theoretical viewpoint. The presentation builds on the following publications [3], [1] and [2].

  1. Brændeland, G., Refsdal, A., Stølen, K.: Modular analysis and modelling of risk scenarios with dependencies. J. Syst. Softw. 83(10), 1995–2013 (2010)
  2. Brændeland, G., Refsdal, A., Stølen, K.: A denotational model for component-based risk analysis. Research report 363, University of Oslo (2011)
  3. Lund, M.S., Solhaug, B., Stølen, K.: Model-Driven Risk Analysis – The CORAS Approach. Springer (2011)

 

Our sponsors:

The Research Council of Norway      The Department of Informatics      The University of Oslo       Visit Oslo