Abstract Specification in Object-Z and CSP

2002 ◽  
pp. 108-119 ◽  
Author(s):  
Graeme Smith ◽  
John Derrick
Keyword(s):  
Abstract Specification

Formalizing Timed BPEL by D-LOTOS

2014 ◽  
Vol 5 (2) ◽  
pp. 1-21
Author(s):  
Imed Eddine Chama ◽  
Nabil Belala ◽  
Djamel Eddine Saidouni
Keyword(s):  
Web Services ◽  
Formal Verification ◽  
Real Time ◽  
Formal Representation ◽  
The Real ◽  
True Concurrency ◽  
Transformation Approach ◽  
Abstract Specification

Different standards and languages are proposed in the literature to model the composition of Web services. Unfortunately these languages are essentially syntactic and thus contain much ambiguity and inconsistency. In addition, the formal verification of the proposed languages is impossible. In this paper, the authors propose a transformation approach allowing the formal representation, analysis and refinement of Web services compositions. Both timed constraints and the durations of interactions between these services are taken into account. The authors present a mapping from Web services described in the BPEL language to an abstract specification written in the real-time language D-LOTOS which is based on true-concurrency semantics.

Pointwise extensions of GSOS-defined operations

2011 ◽  
Vol 21 (2) ◽  
pp. 321-361 ◽  
Author(s):  
HELLE HVID HANSEN ◽  
BARTEK KLIN
Keyword(s):  
Operational Semantics ◽  
Infinite Trees ◽  
Structural Operational Semantics ◽  
Algebraic Operations ◽  
Abstract Specification

Final coalgebras capture system behaviours such as streams, infinite trees and processes. Algebraic operations on a final coalgebra can be defined by distributive laws (of a syntax functor Σ over a behaviour functor F). Such distributive laws correspond to abstract specification formats. One such format is a generalisation of the GSOS rules known from structural operational semantics of processes. We show that given an abstract GSOS specification ρ that defines operations σ on a final F-coalgebra, we can systematically construct a GSOS specification ρ that defines the pointwise extension σ of σ on a final FA-coalgebra. The construction relies on the addition of a family of auxiliary ‘buffer’ operations to the syntax. These buffer operations depend only on A, so the construction is uniform for all σ and F.

Abstract specification and formalization of an operating system kernel in Z

2011 ◽  
Vol 45 (1) ◽  
pp. 156-160
Author(s):  
Luciano Barreto ◽  
Aline Andrade ◽  
Adolfo Duran ◽  
Caique Lima ◽  
Ademilson Lima
Keyword(s):  
Operating System ◽  
Abstract Specification

scholarly journals An Abstract Specification Language for Static Program Analysis

2009 ◽  
Vol 254 ◽  
pp. 181-197 ◽  
Author(s):  
Michael Vistein ◽  
Frank Ortmeier ◽  
Wolfgang Reif ◽  
Ralf Huuck ◽  
Ansgar Fehnker
Keyword(s):  
Program Analysis ◽  
Specification Language ◽  
Static Program Analysis ◽  
Abstract Specification

scholarly journals Specification and Verification of Concurrent Programs

1979 ◽  
Vol 8 (94) ◽  
Author(s):  
Jørgen Staunstrup
Keyword(s):  
Specification Language ◽  
New Technique ◽  
Concurrent Programs ◽  
Writing Program ◽  
State Changes ◽  
Key Features ◽  
Specification And Verification ◽  
A New Technique ◽  
Abstract Specification

A new technique for specifying and verifying concurrent programs is presented. A specification language for writing abstract specifications of concurrent programs is proposed. Key features of the specification language are means for writing program states as partial histories, for structuring specifications, and for specifying state changes by transition commands. Properties of a program are verified from the abstract specification and not from the implementation.

Sign in / Sign up

Export Citation Format

Share Document