IFM
2010
Springer
13 years 10 months ago
2010
Springer
Abstract. The Operational Transformation (OT) approach, used in many collaborative editors, allows a group of users to concurrently update replicas of a shared object and exchange ...
IFM
2010
Springer
13 years 10 months ago
2010
Springer
Though program verification is known and has been used for decades, the verification of a complete computer system still remains a grand challenge. Part of this challenge is the in...
IFM
2010
Springer
13 years 10 months ago
2010
Springer
Abstract. Event-B provides us with a powerful framework for correctby-construction system development. However, while developing dependable systems we should not only guarantee the...
IFM
2010
Springer
13 years 10 months ago
2010
Springer
In this paper we describe techniques for the specification and verification of model transformations using a combination of UML and formal methods. The use of UML 2 notations to s...
IFM
2010
Springer
13 years 10 months ago
2010
Springer
Handling changes to programs and specifications efficiently is a particular challenge in formal software verification. Change impact analysis is an approach to this challenge where...
IFM
2010
Springer
13 years 10 months ago
2010
Springer
Safe is a first-order eager functional language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts...
IFM
2010
Springer
13 years 11 months ago
2010
Springer
A Data Sharing Agreement (DSA) is a contract among two or more principals regulating how they share data. Agreements are usually represented as a set of clauses expressed using the...
IFM
2010
Springer
13 years 11 months ago
2010
Springer
This paper presents initial results of research aimed at developing methods and tools for multidisciplinary collaborative development of dependable embedded systems. We focus on th...
IFM
2010
Springer
13 years 11 months ago
2010
Springer
We present a logical framework that is able to deal with variability in product family descriptions. The temporal logic MHML is based on the classical Hennessy–Milner logic with ...
IFM
2010
Springer
13 years 11 months ago
2010
Springer
Event-B has emerged as one of the dominant state-based formal techniques used for modelling control-intensive applications. Due to the blocking semantics of events, their ordering ...