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.
First International Conference, FASE'98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98 Lisbon, Portugal, March 28 – April 4, 1998 Proceedings
Once a farmer and his friend were sitting at a battered kitchen table. The farmer said, “It's time for the mule's lesson.” Out they went into the yard. The farmer picked up a thick tree branch lying on the ground. He walked up to the mule and hit it over the head so hard the branch shattered. The mule staggered. His friend's jaw dropped. The friend said, “You can't teach a mule a lesson like that...
The purpose of this paper is to make a number of points about the selection of topics, research style, and dissemination of ideas. The writing style chosen is to present past personal decisions which might be regarded as technical or strategic mistakes and to indicate what positive messages can be derived from the experiences.
A critical issue for complex component-based systems design is the modeling and analysis of architecture. One of the complicating factors in developing architectural models is accounting for systems whose architecture changes dynamically (during run time). This is because dynamic changes to architectural structure may interact in subtle ways with on-going computations of the system. In this...
Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques...
AORTA has been proposed as an implementable real-time algebra for concurrent systems where event times, rather than values of data, are critical. In this paper we discuss an extension to AORTA to include a formal data model, allowing integration with a variety of modelbased data specification languages. An example is given using VDM with AORTA to define a time-critical system with important data attributes,...
In this paper we introduce a formal approach for the specification of safety-critical embedded systems. The specification formalisms Z and statecharts are integrated under a suitable structural model. The combined approach uses the advantages of the formalisms while avoiding their disadvantages. The different formalisms yield different, compatible views on the system: the functional view describing...
The application of formal techniques can contribute much to the quality of software, which is of utmost importance for safety-critical embedded systems. These techniques, however, are not easy to apply. In particular, methodological guidance is often unsatisfactory. We address this problem by the concept of an agenda. An agenda is a list of activities to be performed for solving a task in software...
Algebra transformation systems are introduced as formal models of components of open distributed systems. They are given by a transition graph modelling the control flow and partial algebras and method expressions modelling the data states and their transformations. According to this two-level structure they cover both labelled transition systems and rule based specification approaches, corresponding...
In component-based development, object-oriented modelling notations such as UML are being proposed as a way of providing richer specifications of components. Much more so than in bespoke software development, this requires a high level of precision coupled with sufficient expressive power. Expressive power is delivered by adding textual annotations, such as invariants, pre & post conditions, to...
A loose semantics for graph transformation rules which has been developed recently is used in this paper for the compositional verification of specifications. The main conceptual tool here is the notion of view, that is, an incomplete specification describing only a certain aspect of the overall system. A view anticipates the (potential) behavior of the complete system by its loose semantics. This...
We reflect on our experiences from work on the design and semantic underpinnings of Extended ML, a specification language which supports the specification and formal development of Standard ML programs. Our aim is to isolate problems and issues that are intrinsic to the general enterprise of designing a specification language for use with a given programming language. Consequently the lessons learned...
For reuse in concurrent object-oriented languages we present a set of reuse constructs. We give criteria for relations between classes that can be implemented by those reuse constructs, characterize the properties inherited via the constructs and explore that we have not only constructs but concepts for reuse. We demonstrate the concepts and constructs with the object-oriented concurrent language...
We present an environment supporting the flexible and application-specific construction of design plans, which avoids the insurgence of unsuccessful design plans at design time, and is thus backtracking-free. During a planning phase the collection of all complete, executable design plans is automatically synthesized on the basis of simple constraint-like specifications and the library of available...
Model-checking is now widely recognised as an efficient method for analysing computer system properties, such as deadlock-freedom. Its practical applicability is due to existing automatic tools which deal with tedious proofs. Another increasingly research area is formal language integration where the capabilities of each language are used to capture precisely some aspects of a system. In this paper...
The concept of rule-based modification developed in the area of algebraic graph transformations and high-level replacement systems has recently shown to be a powerful concept for vertical stucturing of Petri nets. This includes low-level and high-level Petri nets, especially algebraic high-level nets which can be considered as an integration of algebraic specifications and Petri nets. In a large case...
We present new techniques for formally modeling arbitrary network topologies and control-flow schemes, applicable to high-speed networks. A novel induction technique suitable for process algebraic, finite-state machine techniques is described which can be used to verify end-to-end properties of certain arbitrarily configured networks. We also present a formal model of an algorithm for regulating burstiness...
We describe a case study where novel program analysis technology has been used to pinpoint a subtle bug in a formally developed control program for an embedded system. The main technology amounts to first defining a process algebra (called behaviours) suited to the programming language used (in our case CML) and secondly to devise an annotated type and effect system for extracting behaviours from...
We show how to use high-level synchronization constraints, written in a version of monadic second-order logic on finite strings, to synthesize safety controllers for interactive web services. We improve on the naÏve runtime model to avoid state-space explosions and to increase the flow capacities of services.
We present a Statecharts dialect with only three syntactic constructs and a semantics that is not restricted to describe reactive systems on an implementation level but allows to model them on an abstract, more specification oriented stage, where design alternatives are still left open. We give a refinement calculus with rules that tell the designer how to come from the abstract specification to the...
Human computer interaction can be specified successfully using the concept of information resources and the formal notation of graph grammars. In order to achieve a precise and continuous specification process between the requirements and design stages, however, a suitable strategy for refining abstract specifications into more concrete ones correctly and consistently is highly necessary. In...
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.