Formal Verification of a Subset of UML Diagrams

We introduce an approach that deals with the verification of UML collaboration and sequence diagrams in respect to the objects internal behaviors which are commonly represented by state machine diagrams. The approach is based on the translation of theses diagrams to Maude specifications. In fact, Maude is a declarative programming language, an executable formal specification language, and also a formal verification system, which permit the achievement of the approach goals. We define in details the rules of translating UML diagrams elements into their corresponding Maude specifications. We present the algebraic structures that represent the OR-States and the AND-states in a state machine diagram, and the structure that represents the collaboration and the sequence diagrams. Also, we explain the mechanism of the execution and the verification of the translated specification, which is based on rewriting logics rules.

Download Full-text

Formal Verification of a Subset of UML Diagrams

Computer Engineering ◽

10.4018/978-1-61350-456-7.ch411 ◽

2012 ◽

pp. 948-958

Author(s):

Allaoua Chaoui ◽

Okba Tibermacine ◽

Amer R. Zerek

Keyword(s):

Formal Verification ◽

Programming Language ◽

Formal Specification ◽

State Machine ◽

Declarative Programming ◽

Sequence Diagrams ◽

Uml Diagrams ◽

Approach Goals ◽

Formal Specification Language ◽

State Machine Diagram

Download Full-text

MODEL AND VERIFICATION OF WS-CDL BASED ON UML DIAGRAMS

International Journal of Software Engineering and Knowledge Engineering ◽

10.1142/s0218194010005092 ◽

2010 ◽

Vol 20 (08) ◽

pp. 1119-1149 ◽

Cited By ~ 2

Author(s):

PENGCHENG ZHANG ◽

HENRY MUCCINI ◽

YUELONG ZHU ◽

BIXIN LI

Keyword(s):

Unified Modeling Language ◽

State Machine ◽

Underlying Structure ◽

Unified Modeling ◽

Industry Standard ◽

Modeling Analysis ◽

Uml Class Diagram ◽

Uml Diagrams ◽

Uml Sequence Diagram ◽

State Machine Diagram

The Web Services Choreography Description Language (WS-CDL) is a specification developed by the W3C and can be viewed as a blueprint for the development of end-point services. Consequently, it is worth providing a systematic approach for its modeling, analysis and verification. The Unified Modeling Language (UML) is an industry standard for modeling. Applying UML to model WS-CDL is obviously a promising solution to bring together academics and practitioners through a unique standard language. In this paper, we propose to use different UML diagrams to model WS-CDL. UML Component Diagram is used to model the underlying structure of WS-CDL. UML Sequence Diagram is utilized to model the activities in WS-CDL. UML State Machine Diagram is utilized to model the behaviors of each role participating in a WS-CDL specification. We then enrich the UML State Machine Diagram with data by the use of UML Class Diagram. Given the UML specification of WS-CDL, we then provide a systematic way of formally analyzing and verifying WS-CDL against desired properties. Some experiments show that our approach can verify structural, behavioral and data properties in a middle-scale data-enriched WS-CDL specification.

Download Full-text

USING OCL IN THE FORMAL SPECIFICATION OF THE LIBRARY STANDARDS

International Journal of Software Engineering and Knowledge Engineering ◽

10.1142/s0218194013500101 ◽

2013 ◽

Vol 23 (03) ◽

pp. 341-359 ◽

Cited By ~ 1

Author(s):

GORDANA RUDIĆ ◽

BOJANA DIMIĆ SURLA

Keyword(s):

Programming Language ◽

Data Model ◽

Formal Specification ◽

Source Code ◽

Specification Language ◽

Object Constraint Language ◽

Formal Approach ◽

User Input ◽

Constraint Language ◽

Formal Specification Language

The goal of the research was to check whether we can use a formal specification language such as OCL — Object Constraint Language to express all constraints on the library records proposed by the MARC 21 library standard. The main results are the classification and systematization of the constraints on the structure and the content of the MARC records as well as the specification of the constraints on the data model of MARC 21 in OCL. The obtained results are used in the implementation of the editor for MARC records for validation of the user input. The originality of the work is the adoption of the formal approach in specification of the constraints instead of writing source code in programming language.

Download Full-text

Extending Linear Temporal Logic with Clocks to Object-Z

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.513-517.927 ◽

2014 ◽

Vol 513-517 ◽

pp. 927-930

Author(s):

Zhi Cheng Wen ◽

Zhi Gang Chen

Keyword(s):

Real Time ◽

Temporal Logic ◽

Formal Specification ◽

Large Scale ◽

Linear Temporal Logic ◽

Specification Language ◽

Continuous Variables ◽

Real Time System ◽

Software Specification ◽

Formal Specification Language

Object-Z, an extension to formal specification language Z, is good for describing large scale Object-Oriented software specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. Linear temporal logic can describe real-time system, but it can not deal with time variables well and also can not describe formal specification modularly. This paper extends linear temporal logic with clocks (LTLC) and presents an approach to adding linear temporal logic with clocks to Object-Z. Extended Object-Z with LTLC, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.

Download Full-text