Catálogo de publicaciones - libros

’The author of the paper ’Challenges in Software Certification’ on pages 4-18 of this volume, is grateful to his former student, Mr. Marwan Abdeen, for the considerable content quoted from his thesis entitled, ’A Model for the FDA: General Principles of Software Validation’, and from a joint paper entitled, ’FDA: Between Process and Product Evaluation’, co-authored by Mr. Abdeen, Dr. Maibaum and Dr. Kahl.’

is the name of a mathematical (set-theoretic) approach used to develop , be they computerized or not.

is an open tool set devoted to supporting the development of such systems. It contains a modeling database surrounded by various plug-ins: static checker, proof obligation generator, provers, model-checkers, animators, UML transformers, requirement document handler, etc. The database itself contains the various modeling elements needed to construct discrete transition system models: essentially variables, invariants, and transitions.

As software has invaded more and more areas of everyday life, software certification has emerged as a very important issue for governments, industry and consumers. Existing certification regimes are generally focused on the wrong entity, the development process that produces the artifact to be certified. At best, such an approach can produce only circumstantial evidence for the suitability of the software. For proper scientific evaluation of an artifact, we need to address directly the attributes of the product and their acceptability for certification. However, the product itself is clearly not enough, as we need other artifacts, like requirements specifications, designs, test documentation, correctness proofs, etc. We can organise these artifacts using a simple, idealised process, in terms of which a manufacturer’s own process can be “faked”. The attributes of this idealised process and its products can be modelled, following the principles of Measurement Theory, using the product/process modelling method first introduced by Kaposi.

Monitoring and fault diagnosis are core management tasks for deployed industrial systems. Diagnostic reasoning is closely related to reasoning about implementation correctness. A framework to support the integration of both reasoning tasks is introduced. Many well known formal methods for stepwise program refinement are shown to be compatible with the framework. Compatibility is achieved by treating a formal development as a hierarchical model of the implemented system and then adapting model-based reasoning techniques.

We present a formal, tool-supported approach to the design and maintenance of access control policies expressed in the eXtensible Access Control Markup Language (XACML). Our aim is to help developers evaluate the consequences of policy decisions in complex situations where security requirements change and access decisions may depend on the external dynamic environment. The approach applies the model-oriented specification language from the Vienna Development Method (VDM++). An executable formal model of XACML access control is presented in VDM++. The use of the model to analyse and revise both policies and requirements on the environment is illustrated through an example. An approach to the practical problem of analysing access control in virtual organisations with dynamic membership and goals is proposed.

One of the challenges for designing multi-agent systems is how to capture and reason about agent knowledge and knowledge evolution in a highly abstract and modular way. Hence it is very desirable to have a generic framework in which such systems can be conveniently specified and the properties verified under one umbrella. As a classical reasoning support, the model checking technique has proved to be applicable for systems of reasonable size. However current model checkers for epistemic logics suffer from the state explosion problem and their inability to handle infinite state problems. Prototype Verification System (PVS) is an environment for the development of formal specifications. It integrates a highly expressive specification language and a well supported theorem prover. In this paper, we demonstrate our attempt towards mechanizing epistemic logic reasoning by building a formal, sound and complete verification framework in PVS for reasoning about a spectrum of (dynamic) epistemic logics.

Adaptation is important in dependable embedded systems to cope with changing environmental conditions. However, adaptation significantly complicates system design and poses new challenges to system correctness. We propose an integrated model-based development approach facilitating intuitive modelling as well as formal verification of dynamic adaptation behaviour. Our modelling concepts ease the specification of adaptation behaviour and improve the design of adaptive embedded systems by hiding the increased complexity from the developer. Based on a formal framework for representing adaptation behaviour, our approach allows to employ theorem proving, model checking as well as specialised verification techniques to prove properties characteristic for adaptive systems such as stability.

Simulink is popular in industry for modeling and simulating embedded systems. It is deficient to handle requirements of high-level assurance and timing analysis. Previously, we showed the idea of applying Timed Interval Calculus (TIC) to complement Simulink. In this paper, we develop machine-assisted proof support for Simulink models represented in TIC. The work is based on a generic theorem prover, Prototype Verification System (PVS). The TIC specifications of both Simulink models and requirements are transformed to PVS specifications automatically. Verification can be carried out at interval level with a high level of automation. Analysis of continuous and discrete behaviors is supported. The work enhances the applicability of applying TIC to cope with complex Simulink models.

VeSTA is a push-button tool for checking the correct integration of a component in an environment, for component-based timed systems. By correct integration, we mean that the local properties of the component are preserved when this component is merged into an environment. This correctness is checked by means of a so-called divergence-sensitive and stability-respecting timed -simulation, ensuring the preservation of all linear timed properties expressed in the logical formalism M (Metric Interval Temporal Logic), as well as strong non-zenoness and deadlock-freedom. The development of the tool was guided by the architecture of the O-K tool. This allows, as additional feature, an easy connection of the models considered in VeSTA to the O-C verification platform, and to the o-K tool.

Review and testing are the most practical verification techniques that complement each other, and their effectiveness can be enhanced by utilizing formal specifications. In this paper, we describe a verification method that integrates specification-based review and testing for detecting errors of programs in three phases. First, inspection is used to check whether all the relevant conditions defined in a specification are implemented in the corresponding program and whether there are any errors that may prevent the program from normal termination. Second, testing is carried out to detect errors through dynamic executions of the program and to build a useful relation between the specification and the program. Finally, walkthrough analysis is performed to check whether every functional scenario defined in the specification is correctly implemented by the traversed execution paths in the program and whether any untraversed paths exist and are desired. We present an example to show how our method is applied in practice.