CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

An Operational Semantics for Weak PSL

Koen Claessen (Institutionen för datavetenskap, Formella metoder ; Institutionen för datavetenskap, Funktionell programmering) ; Johan Mårtensson
Lecture Notes in Computer Science (0302-9743). Vol. 3312 (2004), p. 337-351.
[Artikel, refereegranskad vetenskaplig]

Extending linear temporal logic by adding regular expressions increases its expressiveness. However, as for example, problems in recent versions of Accellera's Property Specification Language (PSL) as well as in OpenVera's ForSpec and other property languages show, it is a non-trivial task to give a formal denotational semantics with desirable properties to the resulting logic. In this paper, we argue that specifying an operational semantics may be helpful in guiding this work, and as a bonus leads to an implementation of the logic for free. We give a concrete operational semantics for Weak PSL, which is the safety property subset of PSL. We also propose a denotational semantics which we show to be equivalent to the operational one. This semantics is inspired by a new denotational semantics proposed in recent related work.


Proceedings in: 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD) Location: Austin, TX Date: NOV 15-17, 2004



Denna post skapades 2006-10-09. Senast ändrad 2013-07-04.
CPL Pubid: 2545

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap, Formella metoder (2002-2004)
Institutionen för datavetenskap, Funktionell programmering (2002-2004)

Ämnesområden

Information Technology

Chalmers infrastruktur