Catálogo de publicaciones - libros
Integrated Formal Methods: 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007. Proceedings
Jim Davies ; Jeremy Gibbons (eds.)
En conferencia: 6º International Conference on Integrated Formal Methods (IFM) . Oxford, UK . July 2, 2007 - July 5, 2007
Resumen/Descripción – provisto por la editorial
No disponible.
Palabras clave – provistas por la editorial
No disponibles.
Disponibilidad
Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
---|---|---|---|---|
No detectada | 2007 | SpringerLink |
Información
Tipo de recurso:
libros
ISBN impreso
978-3-540-73209-9
ISBN electrónico
978-3-540-73210-5
Editor responsable
Springer Nature
País de edición
Reino Unido
Fecha de publicación
2007
Información sobre derechos de publicación
© Springer-Verlag Berlin Heidelberg 2007
Cobertura temática
Tabla de contenidos
Unifying Theories of Objects
Michael Anthony Smith; Jeremy Gibbons
We present an approach to modelling Abadi-Cardelli-style object calculi as Unifying Theories of Programming (UTP) designs. Here we provide a core object calculus with an operational semantics, and a corresponding UTP model with a denotational semantics. For clarity, the UTP model is defined in terms of an operand stack, which is used to store the results of subprograms. Models of a less operational nature are briefly discussed. The consistency of the UTP model is demonstrated by a structural induction proof over the operations of the core object calculus. Overall, our UTP model is intended to provide facilities for encoding both object-based and class-based languages.
Pp. 599-618
Non-interference Properties for Data-Type Reduction of Communicating Systems
Tobe Toben
An increasing interest in “Systems of Systems”, that is, Systems comprising a varying number of interconnected sub-systems, raises the need for automated verification techniques for dynamic process creation and a changing communication topology. In previous work, we developed a verification approach that is based on finitary abstraction via Data-Type Reduction. To be effective in practice, the abstraction has to be complemented by non-trivial assumptions about valid communication behaviour, so-called non-interference lemmata.
In this paper, we mechanise the generation and validation of these kind of non-interference properties by integrating ideas from communication observation and counter abstraction. We thereby provide a fully automatic procedure to substantially increase the precision of the abstraction.
We explain our approach in terms of a modelling language for dynamic communication systems, and use a running example of a car platooning system to demonstrate the effectiveness of our extensions.
Pp. 619-638
Co-simulation of Distributed Embedded Real-Time Control Systems
Marcel Verhoef; Peter Visser; Jozef Hooman; Jan Broenink
Development of computerized embedded control systems is difficult because it brings together systems theory, electrical engineering and computer science. The engineering and analysis approaches advocated by these disciplines are fundamentally different which complicates reasoning about e.g. performance at the system level. We propose a light-weight approach that alleviates this problem to some extent. An existing formal semantic framework for discrete event models is extended to allow for consistent co-simulation of continuous time models from within this framework. It enables integrated models that can be checked by simulation in addition to the verification and validation techniques already offered by each discipline individually. The level of confidence in the design can now be raised in the very early stages of the system design life-cycle instead of postponing system-level design issues until the integration and test phase is reached. We demonstrate the extended semantic framework by co-simulation of VDM++ and bond-graph models on a case study, the level control of a water tank.
Pp. 639-658