Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import device.
MCU: Micro Controller Unit
Module MCU.
Parameter t:
Type.
Parameter init:
t.
End MCU.
DEV: Peripherals
Module DEV <:
DEV_Sig.
Device state, and initial state
Parameter t :
Type.
Parameter init :
t.
Device operations interface
Parameter ops_query:
Type.
Parameter ops_response:
ops_query ->
Type.
Parameter op_sem:
forall q:
ops_query,
t ->
ops_response q ->
t ->
Prop.
Equivalence relation on device states. In the paper, we simplify
the presentation, and we abstract from that equivalence
relation, using bare equality.
Parameter equiv :
relation t.
Parameter equiv_equiv:
equivalence t equiv.
Parameter op_sem_equiv:
forall op_q op_r dev1 dev2 dev3 dev4,
op_sem op_q dev1 op_r dev2 ->
equiv dev1 dev3 ->
op_sem op_q dev3 op_r dev4 ->
equiv dev2 dev4.
Reflexive transitive closure of opsem
Definition ops := {
q:
ops_query &
ops_response q }.
Inductive ops_sem :
list ops ->
t ->
t ->
Prop :=
|
ops_sem_nil:
forall dev,
ops_sem []
dev dev
|
ops_sem_trans:
forall o ol dev1 dev2 dev3,
op_sem (
projT1 o)
dev1 (
projT2 o)
dev2 ->
ops_sem ol dev2 dev3 ->
ops_sem (
o::
ol)
dev1 dev3.
Lemma ops_sem_equiv :
forall t dev1 dev1',
ops_sem t dev1 dev1' ->
forall dev2 dev2',
equiv dev1 dev2 ->
ops_sem t dev2 dev2' ->
equiv dev1'
dev2'.
Proof.
induction 1 ;
intros.
-
inv H0.
auto.
-
inv H2.
eapply IHops_sem;
eauto.
eapply op_sem_equiv;
eauto.
Qed.
End DEV.
SPEC
Specification of intermittent computing with peripherals.
Axiomatic semantics in which no power loss occurs.
Module SPEC.
Definition trace :=
list DEV.ops.
Inductive mode :=
Usr |
Drv.
Record state :=
STATE {
m :
mode;
c :
MCU.t ;
d :
DEV.t }.
Transition relation
Parameter step :
state ->
trace ->
state ->
Prop.
Axiomatisation of the transition relation
Axiom axiom_usr:
forall mcu dev mcu'
dev'
t,
step (
STATE Usr mcu dev)
t (
STATE Usr mcu'
dev') ->
dev =
dev' /\
t = [].
Axiom axiom_drv:
forall mcu dev mcu'
dev'
t,
step (
STATE Drv mcu dev)
t (
STATE Drv mcu'
dev') ->
DEV.ops_sem t dev dev'.
Axiom axiom_enter:
forall mcu dev mcu'
dev'
t,
step (
STATE Usr mcu dev)
t (
STATE Drv mcu'
dev') ->
dev =
dev' /\
mcu =
mcu' /\
t = [].
Axiom axiom_leave:
forall mcu dev mcu'
dev'
t,
step (
STATE Drv mcu dev)
t (
STATE Usr mcu'
dev') ->
dev =
dev' /\
mcu =
mcu' /\
t = [].
Axiom axiom_equiv:
forall m m'
mcu mcu'
dev1 dev1'
dev2 t,
DEV.equiv dev1 dev2 ->
step (
STATE m mcu dev1)
t (
STATE m'
mcu'
dev1') ->
exists dev2',
step (
STATE m mcu dev2)
t (
STATE m'
mcu'
dev2').
Trace semantics
Definition sem (
t:
trace):
Prop :=
exists s,
run step (
STATE Usr MCU.init DEV.init)
t s.
End SPEC.