atom-0.1.2: A DSL for embedded hard realtime applications.

Language.Atom.Verification

Synopsis

Documentation

data Model Source

A model of a scheduled program for model checking.

model :: Schedule -> [UV] -> [UA] -> ModelSource

Create a model from a scheduled program.

test :: IO ()Source

A list of assertions captured by a model. assertions :: Model -> [Name]

Bounded model checking starting from the initial state. boundedModelChecking :: Model -> Int -> Name -> IO (Maybe Witness)

K-induction model checking given a min and a max k-depth. kInduction :: Model -> Int -> Int -> Name -> IO ()