Oana Florescu, Jpm Jeroen Voeten, BD Bart Theelen et al. · Munich Personal RePEc Archive (Ludwig Maximilian University of Munich) · 2008
The Parallel Object-Oriented Specification Language (POOSL) is an expressive modelling language for hardware/software systems [10]. It was originally defined in [7] as an object-oriented extension of process algebra CCS [6], supporting (conditional) synchronous message passing between (hierarchically structured) asynchronous concurrent processes. Meanwhile, POOSL has been extended with real-time [2] and probabilities [I] to evolve into a powerful general-purpose modelling language accompanied with simulation, analysis and synthesis techniques that scale to large industrial design problems.
Cited by 0
Haughton, Howard, Lano, K · CERN Document Server (European Organization for Nuclear Research) · 1994
Cited by 0
P. J. Whysall, John McDermid · Workshops in computing · 1991
Cited by 15
Tim Clement · Software Engineering Journal · 1995
Cited by 4
José Meseguer · 1994
Abstract : This final report summarizes the research performed for the Office of Naval Research under Contract N00014-90-C-0086 on the topic Object-Oriented Design and Specification. The project began on 1 January 1990 and ended on 31 December 1994. Dr. Jose Meseguer was the project leader. Drs. Patrick Lincoln, and Narciso Martf-Oliet and Mr. Timothy Winkler also worked on the project. Early in the project, an important breakthrough took place with the discovery of rewriting logic, which was then further developed 25, 23, 26. Rewriting logic has proved to be a very flexible multiparadigm logic 27 of great simplicity allowing the unification of equational programming, Horn logic programming, object-oriented programming, and concurrent programming. In particular, a very simple semantics can be given in rewriting logic to concurrent object-oriented programming 24, 29, 28 and to object- oriented databases 33. This is particularly encouraging given that concurrent object-oriented programming and object-oriented databases are disciplines generally considered to lack a precise semantics . Encouraged by these results, a preliminary language design for Maude, a wide-spectrum multiparadigm language based on rewriting logic and containing a subset called Simple Maude that can be efficiently compiled onto a wide variety of parallel machines has been developed 34, 27, 30, 28, 17; and very encouraging experience about its suitability for specifying concurrent systems, AI problems, programming languages, and logics has been gathered 30, 20, 21, 32, 22. In addition, some initial progress has been made on transformation and compilation techniques for the Simple Maude parallel programming sublanguage 17,18.
Cited by 0
Ole-Johann Dahl · 1986
No abstract available.
Cited by 4
Roger Duke, Gordon A. Rose · Queensland's institutional digital repository (The University of Queensland) · 2000
Preface Specification and Object Orientation Graphical Presentatio of Specifications Local vs Central Control Distributed and Mediated Message Passing Dependency and Information Sharing Reliable Behaviour Proving Invariant Properties Polymorphic Inheritance Hierachies Class Union Object Containment Computational Systems Functional Abstraction Semantic Issues of Object-Z Background Notation Glossary of Notation Object-Z Concrete Syntax Further Reading
Cited by 140
Tommaso Bolognesi, John Derrick · IEE Proceedings - Software · 1998
The authors propose a specification style which combines the features and advantages of object-oriented and constraint-oriented system decomposition. A system description is decomposed into data-handling objects, which usually reflect objects and individual operations in the real system, and temporal-ordering constraints, which capture aspects of functionality as behavioural sequences, with a possibility to also introduce entities which blur the distinction between these two extreme cases. Composition is achieved via synchronisation on shared operations: different objects/constraints insisting on an operation express different views on the enabling conditions and effects of that operation. Objects, constraints, and their composition can be formally specified in Object-Z, an object-oriented extension of the Z notation, with pure temporal ordering constraints equivalently expressed as transition graphs. However, expressing object/constraint compositions in Object-Z is cumbersome. This problem is solved by proposing a natural textual notation, called co-expression, which is a most direct description of an object/constraint interconnection graph, and we define a mapping from co-expressions to Object-Z. Thus, specifications in an object/constraint-oriented style can be conveniently written using transition graphs and interconnection diagrams mixed with Object-Z text, and then translated into this language.
Cited by 4
M. Buchanan, Carol Britton · Microprocessing and Microprogramming · 1992
Cited by 0
Tews, Hendrik · Qucosa (Saxon State and University Library Dresden) · 2002
This thesis is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level to pave the way for real world applications of software verification. There are two main contributions of the present thesis: 1. Chapter 3 proposes a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be modelled with these generalised coalgebras. 2. Chapter 4 presents the specification language CCSL (short for Coalgebraic Class Specification Language), its syntax, its semantics, and a prototype compiler that translates CCSL into higher-order logic.
Cited by 1Open access
Maria Naumcheva · HAL (Le Centre pour la Communication Scientifique Directe) · 2022
co-located with the 28th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2022)
Cited by 1Open access
Engels Groenewegen, L. P. J. Groenewegen · 1996
Object-oriented specification mechanisms have become famous for modelling structure and behaviour together in terms of autonomous objects communicating via message passing. However, whereas most object-oriented specification methods are strong in modelling the local behaviour of single objects, they fall short on modelling the coordinated behaviour and collaboration of several objects together. The aim of this paper is to contribute to fill this gap. The paper reports on concepts, language constructs, and experiences with three collaboration formalisms in the area of object-oriented specifications. Keywords object-oriented specification, collaboration, synchronization, cooperation contract 1 INTRODUCTION Due to the high availability of interconnected computers, software systems are no longer restricted to support the work of individuals. Now it becomes more and more common that software systems support the work of groups of somehow interrelated persons, too. Concrete examples of such...
Cited by 0
Ari Jaaksi · Software Practice and Experience · 1995
Abstract This paper presents an object‐oriented approach for the specification of graphical user interfaces. Specification starts with the analysis of the end user's operations. The user interface is then designed on the basis of this analysis. Operation analysis is followed by structure and component specification which presents the dialogue structure of the application and the contents of each dialogue. Visualization produces the final screen layouts, and task specification documents the usage of the user interface for the purpose of creating user's guides. The method presented in this paper makes it easier for a designer to take the end user's needs into account. Still, it does not automatically guarantee good quality user interfaces. The top‐down nature of the method allows the designer to concentrate on the most important aspects of the user interface and split the design procedure into manageable pieces. Also, the visibility of the process allows the designer to communicate with other people while specifying the user interface. This paper connects the method with the object‐oriented specification of entire applications. It briefly explains the connections with object‐oriented analysis and design, and demonstrates how to implement the specified user interface in an object oriented fashion. The approach presented in this paper is being applied in the development of a large network management system with about two million lines of C++ code running in the XII environment. Still, the method does not require the specification being implemented with any specific windowing system. The only requirement is that the user interface is based on graphical elements, such as dialogues, push‐buttons and text fields.
Cited by 10
Wieringa, Roelf J. · University of Twente Research Information · 1998
Cited by 0
Stephen Shaoyi Liao, Jian Ma, Louis Lasoudris · IFIP advances in information and communication technology · 1995
Cited by 1Open access
Grit Denker, Hans-dieter Ehrich · 1995
Reification is a popular technique to reduce complexity of the software design process. This technique has to be re-investigated for the comprehensive objectoriented approach. Object-oriented specifications comprise structure and behavior of systems. Due to this sophisticated idea two kinds of reification appear: data reification and action reification. In this paper we present an approach to incorporate action reification in object-oriented specification. A logic is defined which serves as a domain to translate specifications. Moreover, we define a language for reification and formalize it with the logic. Interpretation structures of this logic are labelled event structures which are introduced briefly and satisfaction of formulas is defined. With an example we explain our ideas of correct reification and establish a reification condition. Finally, we show how data reification is uniformly included in our approach.
Cited by 0
Barrett R. Bryant · 2002
A methodology is proposed for the formal development of software systems from a user's requirements specification in natural language into a complete implementation, proceeding through the steps of formal specification, and detailed design and implementation in an automated manner. Our methodology is based upon the theories of two-level grammar (TLG) and object-oriented design and takes advantage of the existence of several existing software design tools. We develop an iterative transformation process from the natural language specification into the final implementation, with a specification development environment to assist the user, as well as the designer in accomplishing this transformation. Our underlying formal specification methodology may also be used in the final development of the implementation. This methodology is a major advance in object-oriented software development and the software engineering process in general.
Cited by 36
Kevin Lano · Workshops in computing · 1994
Cited by 11
Gunter Saake, Ralf Jungclaus, Hans-Dieter Ehrich · 1991
A basic concept in object-oriented approaches is the notion of object as integrated unit of structure and behavior. Conceptually, objects are modeled as processes of which certain dynamic characteristics of their internal state can be observed using attributes. Objects are the basic units of design. Systems are composed from objects that interact to provide the desired services. In the semantics domain, concepts related to the object-oriented paradigm like interaction, inheritance and object aggregation can be uniformily modelled by object morphisms. In this paper we introduce the language T ROLL to conceptually specify dynamic information systems. T ROLL supports abstract description of temporal evolvement of objects, classification of objects, complex objects, active objects and specialization hierarchies. Additionally, the integration of concepts like modularization support, and component reusability into the T ROLL framework is briefly discussed. 1 Introduction The modeling of com...
Cited by 12
D.K.C. Chan, David J. Harper, Phil Trinder · 2002
This paper presents a formal specification of an object-oriented data model using the Z specification language. The model supports all the essential features found in existing object-oriented data models. More importantly it simultaneously supports multiple inheritance, method overloading together with static type-checking. Formal specification not only helps to overcome the ambiguity problems found in less formal approaches it also allows one to reason about the properties of the model. This specification demonstrates the use of Z as a formal technique in an area where such a definition is greatly needed.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
Cited by 1