Verified Certification of Reachability Checking for Timed Automata
433
1
definition check (L, M ) ≡
2
monadic list all L (λl. do {
3
let S = M l ;
4
let next = succs l S ;
5
monadic list all next (λ(l
, S
). do {
6
xs ← SPEC (λxs. set xs = S
) ;
7
if xs = [] then return True else do {
8
b1 ← return (l
∈ L) ;
9
ys ← SPEC (λxs. set xs = M l
) ;
10
b2 ← monadic list all xs (λx.
11
monadic list ex ys (λy. return (x y))
12
) ;
13
return (b1 ∧ b2)
14
}
15
} )
16
} )
Listing 1.1: Monadic program to check whether a certificate is closed.
– The set of explored states is emitted as a certificate, possibly followed by
compression (see section 4).
– The model, the final state predicate F , the certificate, and a description of
the renaming that was used for the states are passed to the verified certifier.
– The certifier checks that the given renaming is injective, renames the model
accordingly, applies the product construction and checks that the certificate
is admissible.
If the process is successful, we can conclude by Corollary 1 that no “bad” state
(l, s) (i.e. with F l) is reachable symbolically. We will argue that this really implies
that the model is safe in the concrete case of timed automata in section 2.3.
We now lay out how a verified certificate checker that implements said
strategy for an abstract transition system can be constructed in Isabelle/HOL.
Listing 1.1 displays the definition of the core of the checker that checks whether
the certificate is closed in the sense defined above. The program is defined in the
non-determinism monad of the Imperative Refinement Framework (IRF) [20].
Some parts, such as checking set membership or converting a (finite) set to a
list are still left abstract. A non-deterministic specification SPEC Q returns some
value v with Q v.
The body of the program (lines 2-16) iterates over all discrete states in the
certificate L and checks that all corresponding symbolic states are covered. Line
3 retrieves the symbolic states that correspond to discrete state l and in line 4
their symbolic successor states are computed. The result (next) is a list of pairs
of a discrete state and the set of its corresponding symbolic states. The loop
ranging from lines 5 to 15 iterates over this list to ensure that all the successor
states are covered. Given a discrete state l
and a set of symbolic states S
, line 6
first converts it into a list xs that can be iterated over. This turns into a vacuous
433
1
definition check (L, M ) ≡
2
monadic list all L (λl. do {
3
let S = M l ;
4
let next = succs l S ;
5
monadic list all next (λ(l
, S
). do {
6
xs ← SPEC (λxs. set xs = S
) ;
7
if xs = [] then return True else do {
8
b1 ← return (l
∈ L) ;
9
ys ← SPEC (λxs. set xs = M l
) ;
10
b2 ← monadic list all xs (λx.
11
monadic list ex ys (λy. return (x y))
12
) ;
13
return (b1 ∧ b2)
14
}
15
} )
16
} )
Listing 1.1: Monadic program to check whether a certificate is closed.
– The set of explored states is emitted as a certificate, possibly followed by
compression (see section 4).
– The model, the final state predicate F , the certificate, and a description of
the renaming that was used for the states are passed to the verified certifier.
– The certifier checks that the given renaming is injective, renames the model
accordingly, applies the product construction and checks that the certificate
is admissible.
If the process is successful, we can conclude by Corollary 1 that no “bad” state
(l, s) (i.e. with F l) is reachable symbolically. We will argue that this really implies
that the model is safe in the concrete case of timed automata in section 2.3.
We now lay out how a verified certificate checker that implements said
strategy for an abstract transition system can be constructed in Isabelle/HOL.
Listing 1.1 displays the definition of the core of the checker that checks whether
the certificate is closed in the sense defined above. The program is defined in the
non-determinism monad of the Imperative Refinement Framework (IRF) [20].
Some parts, such as checking set membership or converting a (finite) set to a
list are still left abstract. A non-deterministic specification SPEC Q returns some
value v with Q v.
The body of the program (lines 2-16) iterates over all discrete states in the
certificate L and checks that all corresponding symbolic states are covered. Line
3 retrieves the symbolic states that correspond to discrete state l and in line 4
their symbolic successor states are computed. The result (next) is a list of pairs
of a discrete state and the set of its corresponding symbolic states. The loop
ranging from lines 5 to 15 iterates over this list to ensure that all the successor
states are covered. Given a discrete state l
and a set of symbolic states S
, line 6
first converts it into a list xs that can be iterated over. This turns into a vacuous