The paper appeared in TAP'12. Here's a link to the paper and the talk.

The system has been implemented in Haskell and is applied in some real-world projects. Some of the Haskell source code will be made publicly available (later in the year).

skip to main |
skip to sidebar
## Monday, 4 June 2012

###
Constructive Finite Trace Analysis with Linear Temporal Logic

## Labels

We consider linear temporal logic (LTL) for run-time testing
over limited time periods. The technical challenge
is to check if the finite trace produced by the system
under test matches the LTL property.
We present a constructive solution to this problem.
Our finite trace LTL matching algorithm
yields a proof explaining why a match exists.
We apply our constructive LTL matching
method to check if LTL properties are sufficiently covered
by traces resulting from tests.

The paper appeared in TAP'12. Here's a link to the paper and the talk.

The system has been implemented in Haskell and is applied in some real-world projects. Some of the Haskell source code will be made publicly available (later in the year).

Subscribe to:
Post Comments (Atom)

- actor
- boosting
- communicating FA
- concurrency
- constraint handling rules
- control
- coordination
- dsl
- erlang
- formal methods
- guards
- haskell
- join
- join pattern
- library
- linear temporal logic
- model-checking
- multi-set rewrite rules
- parallelism
- partial derivatives
- partial evaluation
- proofs are programs
- regular expressions
- software transactional memory
- types
- uppaal

## No comments:

Post a Comment