Software specification techniques

1989 ◽  
Vol 31 (8) ◽  
pp. 451
Author(s):  
K Heerjee
Keyword(s):  
Software Specification ◽  
Specification Techniques

Priority Program SoftSpez and the International INT Workshops “Integration of Software Specification Techniques for Applications in Engineering” (DFG-Schwerpunktprogramm SoftSpez und die internationalen INT-Workshops „Integration von Techniken der Softwarespezifikation für ingenieurwissenschaftliche Anwendungen“)

2005 ◽  
Vol 47 (1) ◽  
Author(s):  
Hartmut Ehrig ◽  
Benjamin Braatz ◽  
Markus Klein
Keyword(s):  
Software Engineering ◽  
Control Systems ◽  
Research Area ◽  
Industrial Control ◽  
German Research Foundation ◽  
Industrial Control Systems ◽  
Software Specification ◽  
German Research ◽  
Specification Techniques ◽  
Priority Program

AbstractThe research area “Integration of Software Specification Techniques for Applications in Engineering” has been subject of the Priority Program SoftSpez of the German Research Foundation (DFG) in the years 1998–2004 and of the international INT workshops as satellite events of the ETAPS conferences in 2000, 2002, and 2004. In this paper, we present an overview of aims, organization, and results of these activities. Moreover, we present an example for the integration of specification techniques in software engineering and industrial control systems developed within the project IOSIP of SoftSpez.

scholarly journals From parametric trace slicing to rule systems

2021 ◽  
Author(s):  
Giles Reger ◽  
David Rydeheard
Keyword(s):  
Runtime Verification ◽  
Specification Languages ◽  
Execution Traces ◽  
Running System ◽  
Proof Of Correctness ◽  
Rule Systems ◽  
The Relationship ◽  
Specification Techniques ◽  
Previous Conference

AbstractParametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for parametric runtime verification. Here we consider the correspondence between trace-slicing automata-based approaches and rule systems. The main contribution is a translation from quantified automata to rule systems, which has been implemented in Scala. This then allows us to highlight the key differences in how the two formalisms handle data, an important step in our wider effort to understand the correspondence between different specification languages for parametric runtime verification. This paper extends a previous conference version of this paper with further examples, a proof of correctness, and an optimisation based on a notion of redundancy observed during the development of the translation.

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