Formal Aspects of Computing
SCIE-ISI SCOPUS (1989-2023)
1433-299X
0934-5043
Cơ quản chủ quản: Association for Computing Machinery (ACM) , ASSOC COMPUTING MACHINERY
Lĩnh vực:
SoftwareTheoretical Computer Science
Các bài báo tiêu biểu
A New Approach to Abstract Syntax with Variable BindingAbstract.
The permutation model of set theory with atoms (FM-sets), devised by Fraenkel and Mostowski in the 1930s, supports notions of ‘name-abstraction’ and ‘fresh name’ that provide a new way to represent, compute with, and reason about the syntax of formal systems involving variable-binding operations. Inductively defined FM-sets involving the name-ab... ... hiện toàn bộ
- 2002
Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checkerAbstract.
Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priori... ... hiện toàn bộ
- 1999
A formal approach to adaptive software: continuous assurance of non-functional requirementsAbstract
Modern software systems are increasingly requested to be adaptive to changes in the environment in which they are embedded. Moreover, adaptation often needs to be performed automatically, through self-managed reactions enacted by the application at run time. Off-line, human-driven changes should be requested only if self-adaptation cannot be achi... ... hiện toàn bộ
Tập 24 Số 2 - Trang 163-186 - 2012
Temporal theories as modularisation units for concurrent system specificationAbstract
In this paper, we bring together the use of temporal logic for specifying concurrent systems, in the tradition initiated by A. Pnueli, and the use of tools from category theory as a means for structuring specifications as combinations of theories in the style developed by R. Burstall and J. Goguen. As a result, we obtain a framework in which syst... ... hiện toàn bộ
- 1992
A Refinement Strategy for CircusAbstract
We present a refinement strategy for
Circus
, which is the combination of Z, CSP, and the refinement calculus in the setting of Hoare and He’s unifying theories of programming. The strategy unifies the theories of refinement for processes and their constituent actions, and provides a... ... hiện toàn bộ
Tập 15 Số 2-3 - Trang 146-181 - 2003
Issues in the design of a parallel object-oriented languageAbstract
This paper discusses the considerations that have played a role in the design of the language POOL2. This language integrates the structuring techniques of object-oriented programming with mechanisms for expressing parallelism. We introduce the basic principles of object-oriented programming and its significance for program development methodolog... ... hiện toàn bộ
Tập 1 Số 1 - Trang 366-411 - 1989
MetateM: An introductionAbstract In this paper a methodology for the use of temporal logic as an executable imperative language is introduced. The approach, which provides a concrete framework, calledMetateM , for executing temporal formulae, is motivated and illustrated through examples. In addition, this introduction provides references to further, more detailed, work r...
Tập 7 Số 5 - Trang 533-549 - 1995
On the lattice of specifications: Applications to a specification methodologyAbstract
In this paper we investigate the lattice properties of the natural ordering between specifications, which expresses that a specification expresses a stronger requirement than another specification. The lattice-like structure that we uncover is used as a basis for a specification methodology.
- 1992
MetateM: An introductionAbstract In this paper a methodology for the use of temporal logic as an executable imperative language is introduced. The approach, which provides a concrete framework, calledMetateM , for executing temporal formulae, is motivated and illustrated through examples. In addition, this introduction provides references to further, more detailed, work r...
Tập 7 Số 5 - Trang 533-549 - 1995
A Formal Semantics of Data Flow Diagrams
Tập 6 - Trang 586-606 - 2012
This paper presents a formal semantics of data flow diagrams as used in Structured Analysis, based on an abstract model for data flow transformations. The semantics consists of a collection of VDM functions, transforming an abstract syntax representation of a data flow diagram into an abstract syntax representation of a VDM specification. Since this transformation is executable, it becomes possibl...... hiện toàn bộ