The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Formal specification methods have not been embraced wholeheartedly by the software development industry. We believe that a large part of industry's reluctance is due to semantic gaps that are encountered when attempting to integrate formal specification with other stages of the software development process. Semantic gaps necessitate a dramatic shift in a programmer's mode of thought, and undergoing...
An important goal of software engineering is to exploit commonalities in system design in order to reduce the complexity of building new systems, support large-scale reuse, and provide automated assistance for system development. A significant roadblock to accomplishing this goal is that common properties of systems are poorly understood. In this paper we argue that formal specification can help solve...
The variants of specification languages used with the Vienna Development Method (VDM) offer a rather expressive notion of types. Higher order function types, recursively defined types, and a notion of union types which does not require injection and projection are all included, not to mention subtypes characterized by arbitrary predicates. Besides this, VDM specifications are in general not...
We provide a rigorous development of a structure sharing unification algorithm from an abstract algorithm of established correctness. This is done by a mixture of transformation and posit- and-prove techniques. From this, some conclusions are drawn about a practical approach to rigorous development and the way in which it should be supported.
Both formal methods and structured methods in software development have disadvantages inherent to the class of methods they belong to. A better method may be composed by taking the best of a formal method and the best of a structured method and constructing one, new method. In this paper two approaches to transforming data flow diagrams, the main system representation resulting from SA, to constructs...
A model-oriented method for algebraic specifications is described, using the design language COLD-1 as notation. The method is based upon standard algebraic concepts, such as equivalence relations, congruence relations and homomorphisms. The method makes a clear distinction between the abstract type being defined and the model used as representation. The advantage of this approach is that the problem...
Fairness abstractions are useful for reasoning about computations of nondeterministic programs. This paper presents proof rules for reasoning about three fairness notions and one safety assumption with an automated theorem prover. These proof rules have been integrated into a mechanization of the Unity logic [8,9] and are suitable for the mechanical verification of concurrent programs. Mechanical...
This paper deals with the specification of communicating systems and their stepwise transformation into occam-like programs. For communicating systems a model similar to Hoare's CSP is used. First a specification language is given, which is particularly suitable for describing communicating systems. A quite simple readiness semantics allows to specify the users' wishes in an exact but easily expressible...
Prototyping formal specifications can help capture accurately the requirements of real-world problems. We present a software system, called EZ, that generates executable prototypes directly from certain Z specifications. We first describe how nonmodular Z specifications can be mapped to search systems in C-Prolog. We then add modularity (schema referencing) and other features. A short comparison is...
High level Petri nets have tokens with values, traditionally called colors, and transitions that produce tokens in a functional way, using the consumed tokens as arguments of the function application. Large nets should be designed in a topdown approach and therefore we introduce a hierarchical net model which combines a data flow diagram technique with a high level Petri net model. We use Z to specify...
The work presented here concerns abstract specification of type checking for a specification language VDM-SL of the Vienna Development Method. Where previous work has focussed on rejection of “obviously” ill-typed specifications we do, in addition, consider acceptance of “obviously” well-typed expressions. The presentation includes essential parts of the definition of several well-formedness...
The notion of behavioural extension is important for system evolution, incremental design and, inheritance in object-orientation. Behavioural extension as relations between CSP processes is investigated. A number of different extension relations are developed motivated by some examples of behavioural extension from the telecoms domain. Each extension relation is characterised in terms of CSP operators...
We consider type universes as examples of regular algebras in the area of the denotational semantics of programming languages. The paper concentrates on our method which was used implicitly in the studies of the domain universes underlying MetaSoft, cf. [BBP90], and BSI/VDM, cf. [TW90]. Technically speaking the method allows to prove that a given algebra, e.g., an algebra of types, is regular...
This paper compares the finitary three-valued logic LPF and the infinitary two-valued logic MPLω, the logics underlying VDM SL and COLD-K. These logics reflect different approaches to reasoning about partial functions and bringing recursive function definitions into proofs. The purpose of the comparison is to acquire insight into the relationship between these approaches. A natural translation from...
A major issue in software engineering is the mastery of sofware design. The increasing distributed programming facilities open lots of new possibilities but make the task of designers more complex. Our work is to contribute to a rational design of real-sized distributable applications. We propose an approach based on the VDM formal method as support for the design phase and based on the Conic distributed...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.