An Extension to Data-Flow-Oriented Formal Specification Language for Specifying Concurrent Software Systems

2010 ◽  
Author(s):  
Yuting Chen ◽  
Shaoying Liu ◽  
Linzhang Wang
Keyword(s):  
Formal Specification ◽  
Data Flow ◽  
Specification Language ◽  
Software Systems ◽  
Concurrent Software ◽  
Formal Specification Language

Integrating Requirements Engineering Techniques and Formal Methods

2005 ◽  
pp. 1555-1559 ◽  
Author(s):  
María Virginia Mauco ◽  
Daniel Riesco
Keyword(s):  
Formal Methods ◽  
Requirements Engineering ◽  
Formal Specification ◽  
Specification Language ◽  
Software Systems ◽  
Formal Development ◽  
Secure Software ◽  
Formal Specification Language

Formal methods help to develop more reliable and secure software systems, and they are increasingly being accepted by industry. The RAISE1 Method (George et al., 1995), for example, is intended for use on real developments, not just toy examples. This method includes a large number of techniques and strategies for formal development and proofs, as well as a formal specification language, the RAISE Specification Language (RSL) (George et al., 1992), and a set of tools (George et al., 2001).

Extending Linear Temporal Logic with Clocks to Object-Z

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.

Sign in / Sign up

Export Citation Format

Share Document