In this paper we describe and compare two methodologies for verifying the correctness of a speculative out-of-order execution system with interrupts. Both methods are deductive (we use PVS) and are based on refinement...
详细信息
ISBN:
(纸本)3540672826
In this paper we describe and compare two methodologies for verifying the correctness of a speculative out-of-order execution system with interrupts. Both methods are deductive (we use PVS) and are based on refinement. the first proof is by direct refinement to a sequential system;the second proof combines refinement with induction over the number of retirement buffer slots.
We present the application of the formal specification language RT-Z, an integration of the model-based specification language Z and the real-time process algebra timed CSP, in the area of safety-critical systems. the...
详细信息
ISBN:
(纸本)3540672613
We present the application of the formal specification language RT-Z, an integration of the model-based specification language Z and the real-time process algebra timed CSP, in the area of safety-critical systems. the characteristics underlying the development of safety-critical systems are identified, and criteria for specification languages to be used in this area are derived. It is demonstrated by means of a case study that RT-Z satisfies these criteria.
We discuss the possibility of a complete system development scheme, supported by semantically rigorous automated tools, within which one can go from an extremely high-level, user-friendly requirement capture method, w...
详细信息
ISBN:
(纸本)3540672613
We discuss the possibility of a complete system development scheme, supported by semantically rigorous automated tools, within which one can go from an extremely high-level, user-friendly requirement capture method, which we call play-in scenarios, to a final implementation. A cyclic process consisting of verification against requirements and synthesis from requirements plays an important part in the scheme, which is not quite as imaginary as it may sound.
this paper presents a technique for verifying specifications which uses the object-oriented state-based language Object-Z. the technique is based upon translation of Object-Z specifications into transition systems. th...
详细信息
ISBN:
(纸本)3540672613
this paper presents a technique for verifying specifications which uses the object-oriented state-based language Object-Z. the technique is based upon translation of Object-Z specifications into transition systems. the translation of Object-Z into a transition system allows one to use established techniques and tools in order to verify the specifications. We present the basis of our translation approach and then illustrate it by a case study. the case study consists in proving properties of our antennae parameter setting problem specification.
We present work on a formal model for the composition of object-oriented modules, or hyperslices, which represent different perspectives on the system being built. Withthe model, we should be able to study existing a...
详细信息
ISBN:
(纸本)3540672613
We present work on a formal model for the composition of object-oriented modules, or hyperslices, which represent different perspectives on the system being built. Withthe model, we should be able to study existing approaches such as subject-oriented programming, as well as extend other object-oriented languages, such as the UML, to accommodate the use of hyperslices. We show here a sample of the specification language that accompanies the formal model, and a small example of its use.
the presentation will cover an overview of the IST-Programme under the 5th Framework of European Research, and will then concentrate on the opportunities of the Key *** Technologies and Infrastructures. the presentati...
详细信息
Withthe advent of comprehensive safety standards for software intensive safety related systems, such as IEC 61508 and its specialisations for particular industry sectors (medical, machinery, process, etc), there is a...
详细信息
ISBN:
(纸本)3540672613
Withthe advent of comprehensive safety standards for software intensive safety related systems, such as IEC 61508 and its specialisations for particular industry sectors (medical, machinery, process, etc), there is a need to establish combinations of techniques which can be used by industry to demonstrate conformance to these standards for particular developments. In this paper we describe one such combination of techniques, involving statecharts and B, which is aimed at reactive control system development. We define strategies for controller decomposition which allow safety invariants to be distributed into subcontroller requirements, and define techniques for the automatic synthesis of controllers from invariants. A case study of a train control system is used to illustrate the ideas.
the problem of consistently engineering large, complex softwaresystems of today is often addressed by introducing new, "improved" models. Examples of such models are architectural, design, structural, behav...
详细信息
ISBN:
(纸本)3540672613
the problem of consistently engineering large, complex softwaresystems of today is often addressed by introducing new, "improved" models. Examples of such models are architectural, design, structural, behavioral, and so forth. Each software model is intended to highlight a particular view of a desired system. A combination of multiple models is needed to represent and understand the entire system. Ensuring that the various models used in development are consistent relative to each other thus becomes a critical concern. this paper presents an approach that integrates and ensures the consistency across an architectural and a number of design models. the goal of this work is to combine the respective strengths of a powerful, specialized (architecture-based) modeling approach with a widely used, general (design-based) approach. We have formally addressed the various details of our approach, which has allowed us to construct a large set of supporting tools to automate the related development activities. We use an example application throughout the paper to illustrate the concepts.
Considerable work has been previously done on testing the static aspects of object-oriented systems. this includes both unit testing of individual objects as well as integration testing which tests whether the static ...
详细信息
ISBN:
(纸本)076950616X
Considerable work has been previously done on testing the static aspects of object-oriented systems. this includes both unit testing of individual objects as well as integration testing which tests whether the static relationships between objects such as inheritance and aggregation have been properly implemented. Little work has been done on testing the dynamic aspects beyond testing individual methods. Important issues such as message sequencing and order of execution of methods and inter-object dynamics have not been adequately addressed in the literature. In this paper, we propose a method of software testing the dynamics of these object oriented systems.
Our approach of rule-based refinement(1) provides a formal description for the stepwise system development based on Petri nets. Rules with a left-hand and a right-hand side allow replacing subnets in a given algebraic...
详细信息
ISBN:
(纸本)3540672613
Our approach of rule-based refinement(1) provides a formal description for the stepwise system development based on Petri nets. Rules with a left-hand and a right-hand side allow replacing subnets in a given algebraic high-level net system. the extension of these rules supports the preservation of system properties. In this paper we extend the preservation of safety properties significantly. We define rules, that introduce new safety properties. In our new approach we propose first the verification of properties at the moment they can be expressed and then their preservation further on. Hence, properties can be checked as long as the system is still small. Moreover, introducing properties allows checking these for the relevant subpart only. Changes that are required later on can be treated the same way and hence preserve the system properties. Hence, we have made a step towards a formal technique for the stepwise system development during analysis and design.
暂无评论