Design for Validation (DeVa)

DeVa (Design for Validation) is an ESPRIT Long Term Research project (No. 20072) in which the department of AI at Ulm cooperates with nine partners and associate members. The project started on Dec. 15, 1995 and has a duration of 36 months.

DeVa aims at providing a set of design guidelines and assessment techniques to simplify and support the validation and certification of dependable distributed real-time systems. The set of closely inter-related results that DeVa plans to provide concern the three main aspects of design for validation, namely understandability, verifiability, and evaluatability. With respect to understandability, DeVa plans to use advanced object-oriented design techniques to deal with logical complexity and tackle dependability issues. With respect to verifiability and evaluatability, the work will be aimed at enriching this design paradigm in order to turn it into an effective "design for validation" paradigm, e.g. via work on (i) disciplined approaches that ensure the testability of the ensuing design, and (ii) evaluations of software architecture trade-offs that encompass the reuse of existing components.

The department of AI at Ulm will mainly contribute to investigation, adaptation, and application of object-oriented approaches to formal modelling and formal verification of dependable systems.

• F.W. von Henke
• E. Canver
• D. Schwier

Project Partners

• CSR, City University, London (UK) - Bev Littlewood
• DRA, Malvern (UK) - Chris Senett
• LAAS-CNRS, Toulouse (F) - Jean-Claude Laprie
• LGL-DI-EPFL (CH) - Didier Buchs
• Department of Computing Science, University of Newcastle upon Tyne (UK) - Brian Randell
  See also the DeVa Home-Page at Newcastle
• Department of Computer Science, University of York (UK) - Alan Burns
  See also the DeVa Page at York

Associate members:

• AIB - Vincotte Nuclear (B) - Pierre-Jacques Courtois
• LRI-CNRS, Université Paris-Sud (F) - Marie-Claude Gaudel
• Real-Time Systems Group, Technische Universität Wien (A) - Hermann Kopetz

Publications

• J. Xu, B. Randell, A. Romanovsky, R. J. Stroud, A. F. Zorzo, E. Canver, F. von Henke: Rigorous Development of an Embedded Fault-Tolerant System Based on Coordinated Atomic Actions, IEEE Trans. on Computers, 2002.
• J. Xu, B. Randell, A. Romanovsky, R. J. Stroud, A. F. Zorzo, E. Canver, F.W. von Henke: Rigorous Development of a Safety-Critical System Based on Coordinated Atomic Actions, FTCS-29, 1999.
• E. Canver, F.W. von Henke: "Formal Development of Object-Based Systems in a Temporal Logic Setting", presented at FMOODS'99, 1999, earlier version available as DeVa Technical Report No.39.
• E. Canver: "Formal Verification of a CAA-Based Design", 1998, also available as DeVa Technical Report No.47.
• D. Schwier, F.W. von Henke: "Mechanical Verification of Clock Synchronization Algorithms", 1998, also available as DeVa Technical Report No.43.
• N. Guelfi, O. Biberstein, D. Buchs, M.-C. Gaudel, E. Canver, F. von Henke, D. Schwier: "Comparison of Object-Oriented Formal Methods", DeVa Technical Report No.27, 1997.
• D. Schwier, F. von Henke, J. Xu, R.J. Stroud, A. Romanovsky, B. Randell: "Formalization of the CA Action Concept Based on Temporal Logic", DeVa Technical Report No.13, 1997.