From 7e9125911f8d36b7dc94605d03942074f7094915 Mon Sep 17 00:00:00 2001 From: codelion Date: Thu, 3 Oct 2013 14:49:52 +0800 Subject: [PATCH] added pacemaker code --- verified_pacemaker/AAI.ltl | 148 +++++++ verified_pacemaker/AAI_H.ltl | 159 +++++++ verified_pacemaker/AAT.ltl | 149 +++++++ verified_pacemaker/ARP.ltl | 125 ++++++ verified_pacemaker/AVD.ltl | 122 ++++++ verified_pacemaker/Distributed_AVD.ltl | 126 ++++++ verified_pacemaker/LRLURLA.ltl | 116 +++++ verified_pacemaker/LRLURLA_R.ltl | 115 +++++ verified_pacemaker/LRLURLA_RC.ltl | 114 +++++ verified_pacemaker/LRLURLV.ltl | 116 +++++ verified_pacemaker/LRLURLV_R.ltl | 114 +++++ verified_pacemaker/LRLURLV_RC.ltl | 114 +++++ verified_pacemaker/PVARP.ltl | 146 +++++++ verified_pacemaker/README.txt | 176 ++++++++ .../Testing_C_Code_Branch_Coverage.pml.ltl | 70 +++ verified_pacemaker/VRP.ltl | 148 +++++++ verified_pacemaker/VVI.ltl | 148 +++++++ verified_pacemaker/VVI_H.ltl | 159 +++++++ verified_pacemaker/VVT.ltl | 148 +++++++ verified_pacemaker/XDD.ltl | 124 ++++++ verified_pacemaker/XDD_H.ltl | 156 +++++++ verified_pacemaker/pacemaker.c | 400 ++++++++++++++++++ verified_pacemaker/pacemaker.h | 31 ++ verified_pacemaker/pacemaker_C_Code.pml | 321 ++++++++++++++ verified_pacemaker/pacemaker_concurrent.pml | 224 ++++++++++ verified_pacemaker/pacemaker_distributed.pml | 243 +++++++++++ verified_pacemaker/pacemaker_sequential.pml | 389 +++++++++++++++++ 27 files changed, 4401 insertions(+) create mode 100644 verified_pacemaker/AAI.ltl create mode 100644 verified_pacemaker/AAI_H.ltl create mode 100644 verified_pacemaker/AAT.ltl create mode 100644 verified_pacemaker/ARP.ltl create mode 100644 verified_pacemaker/AVD.ltl create mode 100644 verified_pacemaker/Distributed_AVD.ltl create mode 100644 verified_pacemaker/LRLURLA.ltl create mode 100644 verified_pacemaker/LRLURLA_R.ltl create mode 100644 verified_pacemaker/LRLURLA_RC.ltl create mode 100644 verified_pacemaker/LRLURLV.ltl create mode 100644 verified_pacemaker/LRLURLV_R.ltl create mode 100644 verified_pacemaker/LRLURLV_RC.ltl create mode 100644 verified_pacemaker/PVARP.ltl create mode 100644 verified_pacemaker/README.txt create mode 100644 verified_pacemaker/Testing_C_Code_Branch_Coverage.pml.ltl create mode 100644 verified_pacemaker/VRP.ltl create mode 100644 verified_pacemaker/VVI.ltl create mode 100644 verified_pacemaker/VVI_H.ltl create mode 100644 verified_pacemaker/VVT.ltl create mode 100644 verified_pacemaker/XDD.ltl create mode 100644 verified_pacemaker/XDD_H.ltl create mode 100644 verified_pacemaker/pacemaker.c create mode 100644 verified_pacemaker/pacemaker.h create mode 100644 verified_pacemaker/pacemaker_C_Code.pml create mode 100644 verified_pacemaker/pacemaker_concurrent.pml create mode 100644 verified_pacemaker/pacemaker_distributed.pml create mode 100644 verified_pacemaker/pacemaker_sequential.pml diff --git a/verified_pacemaker/AAI.ltl b/verified_pacemaker/AAI.ltl new file mode 100644 index 0000000..ff4022a --- /dev/null +++ b/verified_pacemaker/AAI.ltl @@ -0,0 +1,148 @@ +#define p sena == 1 +#define q pula == 0 +#define r avdelay == 0 +#define s lastpacedpulsea == timer + + /* + * Formula As Typed: [] (p -> <> (q && r && s)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> <> (q && r && s))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> <> (q && r && s))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (! ((s)) && (p)))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (! ((s))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 291) +depth 1233: Claim reached state 9 (line 296) +depth 1805: Claim reached state 9 (line 296) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 3172, errors: 0 + 2534 states, stored (3484 visited) + 1898 states, matched + 5382 transitions (= visited+matched) + 3 atomic steps +hash conflicts: 4 (resolved) + +Stats on memory usage (in Megabytes): + 0.271 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.459 actual memory usage for states (unsuccessful compression: 169.54%) + state-vector as stored = 174 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.696 total actual memory usage + +unreached in proctype updatetimers + line 31, "pan.___", state 4, "timer = 0" + line 32, "pan.___", state 5, "avdelay = -(1)" + line 32, "pan.___", state 6, "lastpulse = 0" + line 36, "pan.___", state 12, "timer = 0" + line 37, "pan.___", state 13, "avdelay = -(1)" + line 37, "pan.___", state 14, "lastpacedpulsev = 0" + line 38, "pan.___", state 15, "lastpulse = 0" + line 42, "pan.___", state 21, "avdelay = -(1)" + line 43, "pan.___", state 22, "lastpacedpulsev = 0" + line 57, "pan.___", state 47, "-end-" + (10 of 47 states) +unreached in proctype environment + line 68, "pan.___", state 5, "lastpulse = timer" + line 68, "pan.___", state 6, "avdelay = 0" + line 68, "pan.___", state 8, "lastpulse = timer" + line 68, "pan.___", state 9, "avdelay = 0" + line 68, "pan.___", state 10, "pula = 1" + line 68, "pan.___", state 10, "timer = 0" + line 71, "pan.___", state 14, "avdelay = -(1)" + line 71, "pan.___", state 16, "avdelay = -(1)" + line 71, "pan.___", state 17, "pulv = 1" + line 71, "pan.___", state 17, "timer = 0" + line 82, "pan.___", state 30, "lastpulse = timer" + line 82, "pan.___", state 31, "avdelay = 0" + line 82, "pan.___", state 32, "pula = 1" + line 86, "pan.___", state 36, "avdelay = -(1)" + line 86, "pan.___", state 37, "timer = 0" + line 111, "pan.___", state 73, "-end-" + (14 of 73 states) +unreached in proctype sensor + line 119, "pan.___", state 10, "senv = 1" + line 119, "pan.___", state 11, "pulv = 0" + line 123, "pan.___", state 23, "-end-" + (3 of 23 states) +unreached in proctype pacegen + line 133, "pan.___", state 5, "lastpacedpulsev = timer" + line 133, "pan.___", state 6, "avdelay = -(1)" + line 133, "pan.___", state 7, "pulv = 1" + line 143, "pan.___", state 20, "lastpacedpulsea = timer" + line 143, "pan.___", state 21, "avdelay = 0" + line 143, "pan.___", state 22, "pula = 1" + line 152, "pan.___", state 34, "pulv = 1" + line 152, "pan.___", state 35, "lastpacedpulsev = timer" + line 152, "pan.___", state 36, "avdelay = -(1)" + line 160, "pan.___", state 47, "lastpacedpulsev = timer" + line 160, "pan.___", state 48, "avdelay = -(1)" + line 165, "pan.___", state 55, "lastpacedpulsev = timer" + line 165, "pan.___", state 56, "avdelay = -(1)" + line 165, "pan.___", state 57, "pulv = 1" + line 173, "pan.___", state 69, "lastpacedpulsea = timer" + line 173, "pan.___", state 70, "avdelay = 0" + line 178, "pan.___", state 77, "lastpacedpulsea = timer" + line 178, "pan.___", state 78, "avdelay = 0" + line 178, "pan.___", state 79, "pula = 1" + line 186, "pan.___", state 91, "pulv = 1" + line 186, "pan.___", state 92, "lastpacedpulsev = timer" + line 186, "pan.___", state 93, "avdelay = -(1)" + line 191, "pan.___", state 100, "lastpacedpulsev = timer" + line 191, "pan.___", state 101, "avdelay = -(1)" + line 191, "pan.___", state 102, "pulv = 1" + line 212, "pan.___", state 137, "avdelay = 0" + line 212, "pan.___", state 138, "sensea?_" + line 216, "pan.___", state 142, "lastpacedpulsev = timer" + line 216, "pan.___", state 143, "avdelay = -(1)" + line 216, "pan.___", state 144, "sensev?_" + line 218, "pan.___", state 147, "lastpacedpulsev = timer" + line 218, "pan.___", state 148, "avdelay = -(1)" + line 218, "pan.___", state 149, "pulsev!1" + line 226, "pan.___", state 166, "-end-" + (34 of 166 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 298, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.04 seconds +pan: rate 87100 states/second +pan: avg transition delay 7.4322e-06 usec +0.00user 0.02system 0:00.05elapsed 40%CPU (0avgtext+0avgdata 12928maxresident)k +0inputs+16outputs (0major+848minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/AAI_H.ltl b/verified_pacemaker/AAI_H.ltl new file mode 100644 index 0000000..c100e59 --- /dev/null +++ b/verified_pacemaker/AAI_H.ltl @@ -0,0 +1,159 @@ +#define p sena == 1 +#define q pula == 0 +#define r avdelay == 0 +#define s lastpacedpulsea == timer +#define t responsefactor == 10 + + + /* + * Formula As Typed: [] (p -> <> (q && r && s && t)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> <> (q && r && s && t))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> <> (q && r && s && t))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (((! ((s)) && (p)) || (! ((t)) && (p)))))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (((! ((s))) || (! ((t))))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 385) +depth 1664: Claim reached state 9 (line 390) +depth 1726: Claim reached state 9 (line 390) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 116 byte, depth reached 12407, errors: 0 + 31876 states, stored (46543 visited) + 17465 states, matched + 64008 transitions (= visited+matched) + 4 atomic steps +hash conflicts: 375 (resolved) + +Stats on memory usage (in Megabytes): + 4.013 equivalent memory usage for states (stored*(State-vector + overhead)) + 3.377 actual memory usage for states (compression: 84.17%) + state-vector as stored = 95 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 3.052 memory used for DFS stack (-m100000) + 8.372 total actual memory usage + +unreached in proctype updatetimers + line 45, "pan.___", state 12, "timer = 0" + line 46, "pan.___", state 13, "avdelay = -(1)" + line 46, "pan.___", state 14, "lastpacedpulsev = 0" + line 47, "pan.___", state 15, "lastpulse = 0" + line 51, "pan.___", state 21, "avdelay = -(1)" + line 52, "pan.___", state 22, "lastpacedpulsev = 0" + line 66, "pan.___", state 47, "-end-" + (7 of 47 states) +unreached in proctype environment + line 94, "pan.___", state 34, "lastpulse = timer" + line 94, "pan.___", state 35, "avdelay = 0" + line 94, "pan.___", state 36, "pula = 1" + line 98, "pan.___", state 40, "avdelay = -(1)" + line 98, "pan.___", state 41, "timer = 0" + line 110, "pan.___", state 54, "lastpulse = timer" + line 110, "pan.___", state 55, "avdelay = 0" + line 110, "pan.___", state 56, "timer = 0" + line 114, "pan.___", state 60, "avdelay = -(1)" + line 114, "pan.___", state 61, "timer = 0" + line 122, "pan.___", state 78, "-end-" + (11 of 78 states) +unreached in proctype sensor + line 133, "pan.___", state 19, "senv = 0" + line 133, "pan.___", state 20, "pulv = 0" + line 140, "pan.___", state 41, "-end-" + (3 of 41 states) +unreached in proctype pacegen + line 152, "pan.___", state 6, "pulv = 1" + line 152, "pan.___", state 7, "lastpacedpulsev = timer" + line 152, "pan.___", state 8, "avdelay = -(1)" + line 154, "pan.___", state 14, "pulv = 1" + line 154, "pan.___", state 15, "lastpacedpulsev = timer" + line 154, "pan.___", state 16, "avdelay = -(1)" + line 150, "pan.___", state 17, "(((((mode==VOOR)||(mode==DOOR))||(mode==DDDR))||(mode==VDDR)))" + line 150, "pan.___", state 17, "else" + line 166, "pan.___", state 31, "pula = 1" + line 166, "pan.___", state 32, "lastpacedpulsea = timer" + line 166, "pan.___", state 33, "avdelay = 0" + line 168, "pan.___", state 39, "pula = 1" + line 168, "pan.___", state 40, "lastpacedpulsea = timer" + line 168, "pan.___", state 41, "avdelay = 0" + line 164, "pan.___", state 42, "((((mode==AOOR)||(mode==DOOR))||(mode==DDDR)))" + line 164, "pan.___", state 42, "else" + line 176, "pan.___", state 54, "lastpacedpulsev = timer" + line 176, "pan.___", state 55, "avdelay = -(1)" + line 177, "pan.___", state 57, "responsefactor = 10" + line 186, "pan.___", state 69, "pulv = 1" + line 186, "pan.___", state 70, "lastpacedpulsev = timer" + line 186, "pan.___", state 71, "avdelay = -(1)" + line 188, "pan.___", state 77, "pulv = 1" + line 188, "pan.___", state 78, "lastpacedpulsev = timer" + line 188, "pan.___", state 79, "avdelay = -(1)" + line 184, "pan.___", state 80, "(((mode==VVIR)||(mode==DDIR)))" + line 184, "pan.___", state 80, "else" + line 206, "pan.___", state 107, "pula = 1" + line 206, "pan.___", state 108, "lastpacedpulsea = timer" + line 206, "pan.___", state 109, "avdelay = 0" + line 216, "pan.___", state 130, "pulv = 1" + line 216, "pan.___", state 131, "lastpacedpulsev = timer" + line 216, "pan.___", state 132, "avdelay = -(1)" + line 221, "pan.___", state 139, "lastpacedpulsev = timer" + line 221, "pan.___", state 140, "avdelay = -(1)" + line 221, "pan.___", state 141, "pulv = 1" + line 229, "pan.___", state 153, "pula = 1" + line 229, "pan.___", state 154, "lastpacedpulsea = timer" + line 229, "pan.___", state 155, "avdelay = 0" + line 234, "pan.___", state 162, "lastpacedpulsea = timer" + line 234, "pan.___", state 163, "avdelay = 0" + line 234, "pan.___", state 164, "pula = 1" + line 242, "pan.___", state 176, "avdelay = 0" + line 243, "pan.___", state 178, "responsefactor = 10" + line 248, "pan.___", state 188, "avdelay = -(1)" + line 255, "pan.___", state 199, "pulv = 1" + line 255, "pan.___", state 200, "lastpacedpulsev = timer" + line 255, "pan.___", state 201, "avdelay = -(1)" + line 262, "pan.___", state 217, "-end-" + (46 of 217 states) +unreached in proctype accelerometer + line 294, "pan.___", state 59, "-end-" + (1 of 59 states) +unreached in proctype :init: + (0 of 8 states) +unreached in proctype :never: + line 392, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.783 seconds +pan: rate 59441.89 states/second +pan: avg transition delay 1.2233e-005 usec + +#endif diff --git a/verified_pacemaker/AAT.ltl b/verified_pacemaker/AAT.ltl new file mode 100644 index 0000000..c7d164d --- /dev/null +++ b/verified_pacemaker/AAT.ltl @@ -0,0 +1,149 @@ +#define p sena == 1 +#define q pula == 1 +#define r avdelay == 0 +#define s lastpacedpulsea == timer + + /* + * Formula As Typed: [] (p -> <> (q && r && s)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> <> (q && r && s))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> <> (q && r && s))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (! ((s)) && (p)))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (! ((s))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 291) +depth 1233: Claim reached state 9 (line 296) +depth 1275: Claim reached state 9 (line 296) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 3172, errors: 0 + 2410 states, stored (3236 visited) + 1599 states, matched + 4835 transitions (= visited+matched) + 3 atomic steps +hash conflicts: 3 (resolved) + +Stats on memory usage (in Megabytes): + 0.257 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.361 actual memory usage for states (unsuccessful compression: 140.33%) + state-vector as stored = 141 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.598 total actual memory usage + +unreached in proctype updatetimers + line 31, "pan.___", state 4, "timer = 0" + line 32, "pan.___", state 5, "avdelay = -(1)" + line 32, "pan.___", state 6, "lastpulse = 0" + line 36, "pan.___", state 12, "timer = 0" + line 37, "pan.___", state 13, "avdelay = -(1)" + line 37, "pan.___", state 14, "lastpacedpulsev = 0" + line 38, "pan.___", state 15, "lastpulse = 0" + line 42, "pan.___", state 21, "avdelay = -(1)" + line 43, "pan.___", state 22, "lastpacedpulsev = 0" + line 57, "pan.___", state 47, "-end-" + (10 of 47 states) +unreached in proctype environment + line 68, "pan.___", state 5, "lastpulse = timer" + line 68, "pan.___", state 6, "avdelay = 0" + line 68, "pan.___", state 8, "lastpulse = timer" + line 68, "pan.___", state 9, "avdelay = 0" + line 68, "pan.___", state 10, "pula = 1" + line 68, "pan.___", state 10, "timer = 0" + line 71, "pan.___", state 14, "avdelay = -(1)" + line 71, "pan.___", state 16, "avdelay = -(1)" + line 71, "pan.___", state 17, "pulv = 1" + line 71, "pan.___", state 17, "timer = 0" + line 82, "pan.___", state 30, "lastpulse = timer" + line 82, "pan.___", state 31, "avdelay = 0" + line 82, "pan.___", state 32, "pula = 1" + line 86, "pan.___", state 36, "avdelay = -(1)" + line 86, "pan.___", state 37, "timer = 0" + line 111, "pan.___", state 73, "-end-" + (14 of 73 states) +unreached in proctype sensor + line 119, "pan.___", state 10, "senv = 1" + line 119, "pan.___", state 11, "pulv = 0" + line 123, "pan.___", state 23, "-end-" + (3 of 23 states) +unreached in proctype pacegen + line 133, "pan.___", state 5, "lastpacedpulsev = timer" + line 133, "pan.___", state 6, "avdelay = -(1)" + line 133, "pan.___", state 7, "pulv = 1" + line 143, "pan.___", state 20, "lastpacedpulsea = timer" + line 143, "pan.___", state 21, "avdelay = 0" + line 143, "pan.___", state 22, "pula = 1" + line 152, "pan.___", state 34, "pulv = 1" + line 152, "pan.___", state 35, "lastpacedpulsev = timer" + line 152, "pan.___", state 36, "avdelay = -(1)" + line 160, "pan.___", state 47, "lastpacedpulsev = timer" + line 160, "pan.___", state 48, "avdelay = -(1)" + line 165, "pan.___", state 55, "lastpacedpulsev = timer" + line 165, "pan.___", state 56, "avdelay = -(1)" + line 165, "pan.___", state 57, "pulv = 1" + line 173, "pan.___", state 69, "lastpacedpulsea = timer" + line 173, "pan.___", state 70, "avdelay = 0" + line 178, "pan.___", state 77, "lastpacedpulsea = timer" + line 178, "pan.___", state 78, "avdelay = 0" + line 178, "pan.___", state 79, "pula = 1" + line 186, "pan.___", state 91, "pulv = 1" + line 186, "pan.___", state 92, "lastpacedpulsev = timer" + line 186, "pan.___", state 93, "avdelay = -(1)" + line 191, "pan.___", state 100, "lastpacedpulsev = timer" + line 191, "pan.___", state 101, "avdelay = -(1)" + line 191, "pan.___", state 102, "pulv = 1" + line 212, "pan.___", state 137, "avdelay = 0" + line 212, "pan.___", state 138, "sensea?_" + line 216, "pan.___", state 142, "lastpacedpulsev = timer" + line 216, "pan.___", state 143, "avdelay = -(1)" + line 216, "pan.___", state 144, "sensev?_" + line 218, "pan.___", state 147, "lastpacedpulsev = timer" + line 218, "pan.___", state 148, "avdelay = -(1)" + line 218, "pan.___", state 149, "pulsev!1" + line 226, "pan.___", state 166, "-end-" + (34 of 166 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 298, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.03 seconds +pan: rate 107866.67 states/second +pan: avg transition delay 6.2048e-06 usec +0.00user 0.02system 0:00.07elapsed 34%CPU (0avgtext+0avgdata 12912maxresident)k +0inputs+16outputs (0major+847minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/ARP.ltl b/verified_pacemaker/ARP.ltl new file mode 100644 index 0000000..dea9707 --- /dev/null +++ b/verified_pacemaker/ARP.ltl @@ -0,0 +1,125 @@ +#define p lastpacedpulsea > lastsenseda +#define r (lastpacedpulsea - lastsenseda) > arp + + /* + * Formula As Typed: [] (p -> r) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> r)) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> r)) */ +T0_init: + if + :: (! ((r)) && (p)) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 297) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 104 byte, depth reached 2564, errors: 0 + 1473 states, stored + 3 states, matched + 1476 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.169 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.360 actual memory usage for states (unsuccessful compression: 213.66%) + state-vector as stored = 240 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.598 total actual memory usage + +unreached in proctype updatetimers + line 40, "pan.___", state 12, "timer = 0" + line 41, "pan.___", state 13, "avdelay = -(1)" + line 41, "pan.___", state 14, "lastpacedpulsev = 0" + line 42, "pan.___", state 15, "lastpulse = 0" + line 51, "pan.___", state 28, "avdelay = 0" + line 52, "pan.___", state 29, "lastpacedpulsea = 0" + line 61, "pan.___", state 47, "-end-" + (7 of 47 states) +unreached in proctype environment + line 89, "pan.___", state 34, "lastpulse = timer" + line 89, "pan.___", state 35, "avdelay = 0" + line 89, "pan.___", state 36, "pula = 1" + line 93, "pan.___", state 40, "avdelay = -(1)" + line 93, "pan.___", state 41, "timer = 0" + line 105, "pan.___", state 54, "lastpulse = timer" + line 105, "pan.___", state 55, "avdelay = 0" + line 105, "pan.___", state 56, "timer = 0" + line 109, "pan.___", state 60, "avdelay = -(1)" + line 109, "pan.___", state 61, "timer = 0" + line 117, "pan.___", state 78, "-end-" + (11 of 78 states) +unreached in proctype sensor + line 123, "pan.___", state 3, "sena = 0" + line 123, "pan.___", state 4, "pula = 0" + line 128, "pan.___", state 19, "senv = 0" + line 128, "pan.___", state 20, "pulv = 0" + line 135, "pan.___", state 41, "-end-" + (5 of 41 states) +unreached in proctype pacegen + line 145, "pan.___", state 5, "lastpacedpulsev = timer" + line 145, "pan.___", state 6, "avdelay = -(1)" + line 145, "pan.___", state 7, "pulv = 1" + line 155, "pan.___", state 20, "lastpacedpulsea = timer" + line 155, "pan.___", state 21, "avdelay = 0" + line 155, "pan.___", state 22, "pula = 1" + line 176, "pan.___", state 56, "lastpacedpulsea = timer" + line 176, "pan.___", state 57, "avdelay = 0" + line 181, "pan.___", state 64, "lastpacedpulsea = timer" + line 181, "pan.___", state 65, "avdelay = 0" + line 181, "pan.___", state 66, "pula = 1" + line 189, "pan.___", state 78, "pulv = 1" + line 189, "pan.___", state 79, "lastpacedpulsev = timer" + line 189, "pan.___", state 80, "avdelay = -(1)" + line 194, "pan.___", state 87, "lastpacedpulsev = timer" + line 194, "pan.___", state 88, "avdelay = -(1)" + line 194, "pan.___", state 89, "pulv = 1" + line 202, "pan.___", state 101, "pula = 1" + line 202, "pan.___", state 102, "lastpacedpulsea = timer" + line 202, "pan.___", state 103, "avdelay = 0" + line 207, "pan.___", state 110, "lastpacedpulsea = timer" + line 207, "pan.___", state 111, "avdelay = 0" + line 207, "pan.___", state 112, "pula = 1" + line 215, "pan.___", state 124, "avdelay = 0" + line 218, "pan.___", state 130, "avdelay = -(1)" + line 225, "pan.___", state 141, "pulv = 1" + line 225, "pan.___", state 142, "lastpacedpulsev = timer" + line 225, "pan.___", state 143, "avdelay = -(1)" + line 232, "pan.___", state 159, "-end-" + (29 of 159 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 302, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0.01 seconds +0.00user 0.02system 0:00.07elapsed 27%CPU (0avgtext+0avgdata 12640maxresident)k +0inputs+8outputs (0major+830minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/AVD.ltl b/verified_pacemaker/AVD.ltl new file mode 100644 index 0000000..1602982 --- /dev/null +++ b/verified_pacemaker/AVD.ltl @@ -0,0 +1,122 @@ +#define p avdelay > 0 +#define q avdelay <= avd + + /* + * Formula As Typed: [] (p -> q) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> q)) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> q)) */ +T0_init: + if + :: (! ((q)) && (p)) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 299) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 2558, errors: 0 + 1577 states, stored + 4 states, matched + 1581 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.168 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.360 actual memory usage for states (unsuccessful compression: 213.60%) + state-vector as stored = 223 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.598 total actual memory usage + +unreached in proctype updatetimers + line 31, "pan.___", state 4, "timer = 0" + line 32, "pan.___", state 5, "avdelay = -(1)" + line 32, "pan.___", state 6, "lastpulse = 0" + line 57, "pan.___", state 47, "-end-" + (4 of 47 states) +unreached in proctype environment + line 85, "pan.___", state 34, "lastpulse = timer" + line 85, "pan.___", state 35, "avdelay = 0" + line 85, "pan.___", state 36, "pula = 1" + line 89, "pan.___", state 40, "avdelay = -(1)" + line 89, "pan.___", state 41, "timer = 0" + line 101, "pan.___", state 54, "lastpulse = timer" + line 101, "pan.___", state 55, "avdelay = 0" + line 101, "pan.___", state 56, "timer = 0" + line 114, "pan.___", state 77, "-end-" + (9 of 77 states) +unreached in proctype sensor + line 132, "pan.___", state 37, "-end-" + (1 of 37 states) +unreached in proctype pacegen + line 161, "pan.___", state 34, "pulv = 1" + line 161, "pan.___", state 35, "lastpacedpulsev = timer" + line 161, "pan.___", state 36, "avdelay = -(1)" + line 169, "pan.___", state 47, "lastpacedpulsev = timer" + line 169, "pan.___", state 48, "avdelay = -(1)" + line 174, "pan.___", state 55, "lastpacedpulsev = timer" + line 174, "pan.___", state 56, "avdelay = -(1)" + line 174, "pan.___", state 57, "pulv = 1" + line 182, "pan.___", state 69, "lastpacedpulsea = timer" + line 182, "pan.___", state 70, "avdelay = 0" + line 187, "pan.___", state 77, "lastpacedpulsea = timer" + line 187, "pan.___", state 78, "avdelay = 0" + line 187, "pan.___", state 79, "pula = 1" + line 195, "pan.___", state 91, "pulv = 1" + line 195, "pan.___", state 92, "lastpacedpulsev = timer" + line 195, "pan.___", state 93, "avdelay = -(1)" + line 200, "pan.___", state 100, "lastpacedpulsev = timer" + line 200, "pan.___", state 101, "avdelay = -(1)" + line 200, "pan.___", state 102, "pulv = 1" + line 208, "pan.___", state 114, "pula = 1" + line 208, "pan.___", state 115, "lastpacedpulsea = timer" + line 208, "pan.___", state 116, "avdelay = 0" + line 213, "pan.___", state 123, "lastpacedpulsea = timer" + line 213, "pan.___", state 124, "avdelay = 0" + line 213, "pan.___", state 125, "pula = 1" + line 221, "pan.___", state 137, "avdelay = 0" + line 224, "pan.___", state 143, "lastpacedpulsev = timer" + line 224, "pan.___", state 144, "avdelay = -(1)" + line 227, "pan.___", state 150, "pulv = 1" + line 227, "pan.___", state 151, "lastpacedpulsev = timer" + line 227, "pan.___", state 152, "avdelay = -(1)" + line 234, "pan.___", state 168, "-end-" + (32 of 168 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 304, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0.02 seconds +pan: rate 78850 states/second +pan: avg transition delay 1.265e-05 usec +0.00user 0.01system 0:00.05elapsed 30%CPU (0avgtext+0avgdata 12640maxresident)k +0inputs+8outputs (0major+830minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/Distributed_AVD.ltl b/verified_pacemaker/Distributed_AVD.ltl new file mode 100644 index 0000000..87cdaa7 --- /dev/null +++ b/verified_pacemaker/Distributed_AVD.ltl @@ -0,0 +1,126 @@ +#define p avdelay > 0 +#define q avdelay <= avd +#define r pacedavdelay > 0 +#define s pacedavdelay <= avd + + /* + * Formula As Typed: [] ((p -> q) && (r -> s)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] ((p -> q) && (r -> s))) + * (formalizing violations of the original) + */ + +never { /* !([] ((p -> q) && (r -> s))) */ +T0_init: + if + :: (((! ((q)) && (p) && ((! ((q)) && (p)) || (! ((s)) && (r)))) || (! ((s)) && (r) && ((! ((q)) && (p)) || (! ((s)) && (r)))))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 299) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 2558, errors: 0 + 1577 states, stored + 4 states, matched + 1581 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.168 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.360 actual memory usage for states (unsuccessful compression: 213.60%) + state-vector as stored = 223 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.598 total actual memory usage + +unreached in proctype updatetimers + line 31, "pan.___", state 4, "timer = 0" + line 32, "pan.___", state 5, "avdelay = -(1)" + line 32, "pan.___", state 6, "lastpulse = 0" + line 57, "pan.___", state 47, "-end-" + (4 of 47 states) +unreached in proctype environment + line 85, "pan.___", state 34, "lastpulse = timer" + line 85, "pan.___", state 35, "avdelay = 0" + line 85, "pan.___", state 36, "pula = 1" + line 89, "pan.___", state 40, "avdelay = -(1)" + line 89, "pan.___", state 41, "timer = 0" + line 101, "pan.___", state 54, "lastpulse = timer" + line 101, "pan.___", state 55, "avdelay = 0" + line 101, "pan.___", state 56, "timer = 0" + line 114, "pan.___", state 77, "-end-" + (9 of 77 states) +unreached in proctype sensor + line 132, "pan.___", state 37, "-end-" + (1 of 37 states) +unreached in proctype pacegen + line 161, "pan.___", state 34, "pulv = 1" + line 161, "pan.___", state 35, "lastpacedpulsev = timer" + line 161, "pan.___", state 36, "avdelay = -(1)" + line 169, "pan.___", state 47, "lastpacedpulsev = timer" + line 169, "pan.___", state 48, "avdelay = -(1)" + line 174, "pan.___", state 55, "lastpacedpulsev = timer" + line 174, "pan.___", state 56, "avdelay = -(1)" + line 174, "pan.___", state 57, "pulv = 1" + line 182, "pan.___", state 69, "lastpacedpulsea = timer" + line 182, "pan.___", state 70, "avdelay = 0" + line 187, "pan.___", state 77, "lastpacedpulsea = timer" + line 187, "pan.___", state 78, "avdelay = 0" + line 187, "pan.___", state 79, "pula = 1" + line 195, "pan.___", state 91, "pulv = 1" + line 195, "pan.___", state 92, "lastpacedpulsev = timer" + line 195, "pan.___", state 93, "avdelay = -(1)" + line 200, "pan.___", state 100, "lastpacedpulsev = timer" + line 200, "pan.___", state 101, "avdelay = -(1)" + line 200, "pan.___", state 102, "pulv = 1" + line 208, "pan.___", state 114, "pula = 1" + line 208, "pan.___", state 115, "lastpacedpulsea = timer" + line 208, "pan.___", state 116, "avdelay = 0" + line 213, "pan.___", state 123, "lastpacedpulsea = timer" + line 213, "pan.___", state 124, "avdelay = 0" + line 213, "pan.___", state 125, "pula = 1" + line 221, "pan.___", state 137, "avdelay = 0" + line 224, "pan.___", state 143, "lastpacedpulsev = timer" + line 224, "pan.___", state 144, "avdelay = -(1)" + line 227, "pan.___", state 150, "pulv = 1" + line 227, "pan.___", state 151, "lastpacedpulsev = timer" + line 227, "pan.___", state 152, "avdelay = -(1)" + line 234, "pan.___", state 168, "-end-" + (32 of 168 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 304, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0.02 seconds +pan: rate 78850 states/second +pan: avg transition delay 1.265e-05 usec +0.00user 0.01system 0:00.05elapsed 30%CPU (0avgtext+0avgdata 12640maxresident)k +0inputs+8outputs (0major+830minor)pagefaults 0swaps + + +#endif diff --git a/verified_pacemaker/LRLURLA.ltl b/verified_pacemaker/LRLURLA.ltl new file mode 100644 index 0000000..fb48915 --- /dev/null +++ b/verified_pacemaker/LRLURLA.ltl @@ -0,0 +1,116 @@ +#define p lastpacedpulsea <= maxtime +#define q lastpacedpulsea > 0 +#define r lastpacedpulsea >= mintime + + /* + * Formula As Typed: [] (p && (q -> r)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p && (q -> r))) + * (formalizing violations of the original) + */ + +never { /* !([] (p && (q -> r))) */ +T0_init: + if + :: (((! ((p))) || (! ((r)) && (q) && ((! ((p))) || (! ((r)) && (q)))))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 268) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 922, errors: 0 + 460 states, stored + 1 states, matched + 461 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.049 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.267 actual memory usage for states (unsuccessful compression: 542.77%) + state-vector as stored = 592 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.501 total actual memory usage + +unreached in proctype updatetimers + line 37, "pan.___", state 13, "avdelay = 0" + line 38, "pan.___", state 14, "lastpacedpulsea = 0" + line 42, "pan.___", state 20, "avdelay = (avdelay+100)" + line 47, "pan.___", state 32, "-end-" + (4 of 32 states) +unreached in proctype environment + line 58, "pan.___", state 5, "lastpulse = timer" + line 58, "pan.___", state 6, "avdelay = 0" + line 62, "pan.___", state 12, "avdelay = -(1)" + line 105, "pan.___", state 67, "-end-" + (4 of 67 states) +unreached in proctype sensor + line 117, "pan.___", state 23, "-end-" + (1 of 23 states) +unreached in proctype pacegen + line 137, "pan.___", state 20, "lastpacedpulsea = timer" + line 137, "pan.___", state 21, "avdelay = 0" + line 146, "pan.___", state 35, "lastpacedpulsev = timer" + line 146, "pan.___", state 36, "avdelay = -(1)" + line 146, "pan.___", state 37, "sensev?_" + line 150, "pan.___", state 41, "lastpacedpulsev = timer" + line 150, "pan.___", state 42, "avdelay = -(1)" + line 159, "pan.___", state 56, "lastpacedpulsea = timer" + line 159, "pan.___", state 57, "avdelay = 0" + line 159, "pan.___", state 58, "sensea?_" + line 163, "pan.___", state 62, "lastpacedpulsea = timer" + line 163, "pan.___", state 63, "avdelay = 0" + line 172, "pan.___", state 77, "pulsev!1" + line 172, "pan.___", state 78, "lastpacedpulsev = timer" + line 172, "pan.___", state 79, "avdelay = -(1)" + line 172, "pan.___", state 80, "sensev?_" + line 176, "pan.___", state 84, "lastpacedpulsev = timer" + line 176, "pan.___", state 85, "avdelay = -(1)" + line 185, "pan.___", state 99, "pulsea!1" + line 185, "pan.___", state 100, "lastpacedpulsea = timer" + line 185, "pan.___", state 101, "avdelay = 0" + line 185, "pan.___", state 102, "sensea?_" + line 189, "pan.___", state 106, "lastpacedpulsea = timer" + line 189, "pan.___", state 107, "avdelay = 0" + line 198, "pan.___", state 121, "avdelay = 0" + line 198, "pan.___", state 122, "sensea?_" + line 202, "pan.___", state 126, "lastpacedpulsev = timer" + line 202, "pan.___", state 127, "avdelay = -(1)" + line 202, "pan.___", state 128, "sensev?_" + line 204, "pan.___", state 131, "lastpacedpulsev = timer" + line 204, "pan.___", state 132, "avdelay = -(1)" + line 204, "pan.___", state 133, "pulsev!1" + line 212, "pan.___", state 150, "-end-" + (33 of 150 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 273, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0 seconds +0.00user 0.01system 0:00.03elapsed 50%CPU (0avgtext+0avgdata 12224maxresident)k +0inputs+8outputs (0major+804minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/LRLURLA_R.ltl b/verified_pacemaker/LRLURLA_R.ltl new file mode 100644 index 0000000..abefa6e --- /dev/null +++ b/verified_pacemaker/LRLURLA_R.ltl @@ -0,0 +1,115 @@ +#define p lastpacedpulsea <= maxtime +#define q lastpacedpulsea > 0 +#define r lastpacedpulsea >= sensortime + /* + * Formula As Typed: [] (p && (q -> r)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p && (q -> r))) + * (formalizing violations of the original) + */ + +never { /* !([] (p && (q -> r))) */ +T0_init: + if + :: (((! ((p))) || (! ((r)) && (q) && ((! ((p))) || (! ((r)) && (q)))))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 268) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 922, errors: 0 + 460 states, stored + 1 states, matched + 461 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.049 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.267 actual memory usage for states (unsuccessful compression: 542.77%) + state-vector as stored = 592 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.501 total actual memory usage + +unreached in proctype updatetimers + line 37, "pan.___", state 13, "avdelay = 0" + line 38, "pan.___", state 14, "lastpacedpulsea = 0" + line 42, "pan.___", state 20, "avdelay = (avdelay+100)" + line 47, "pan.___", state 32, "-end-" + (4 of 32 states) +unreached in proctype environment + line 58, "pan.___", state 5, "lastpulse = timer" + line 58, "pan.___", state 6, "avdelay = 0" + line 62, "pan.___", state 12, "avdelay = -(1)" + line 105, "pan.___", state 67, "-end-" + (4 of 67 states) +unreached in proctype sensor + line 117, "pan.___", state 23, "-end-" + (1 of 23 states) +unreached in proctype pacegen + line 137, "pan.___", state 20, "lastpacedpulsea = timer" + line 137, "pan.___", state 21, "avdelay = 0" + line 146, "pan.___", state 35, "lastpacedpulsev = timer" + line 146, "pan.___", state 36, "avdelay = -(1)" + line 146, "pan.___", state 37, "sensev?_" + line 150, "pan.___", state 41, "lastpacedpulsev = timer" + line 150, "pan.___", state 42, "avdelay = -(1)" + line 159, "pan.___", state 56, "lastpacedpulsea = timer" + line 159, "pan.___", state 57, "avdelay = 0" + line 159, "pan.___", state 58, "sensea?_" + line 163, "pan.___", state 62, "lastpacedpulsea = timer" + line 163, "pan.___", state 63, "avdelay = 0" + line 172, "pan.___", state 77, "pulsev!1" + line 172, "pan.___", state 78, "lastpacedpulsev = timer" + line 172, "pan.___", state 79, "avdelay = -(1)" + line 172, "pan.___", state 80, "sensev?_" + line 176, "pan.___", state 84, "lastpacedpulsev = timer" + line 176, "pan.___", state 85, "avdelay = -(1)" + line 185, "pan.___", state 99, "pulsea!1" + line 185, "pan.___", state 100, "lastpacedpulsea = timer" + line 185, "pan.___", state 101, "avdelay = 0" + line 185, "pan.___", state 102, "sensea?_" + line 189, "pan.___", state 106, "lastpacedpulsea = timer" + line 189, "pan.___", state 107, "avdelay = 0" + line 198, "pan.___", state 121, "avdelay = 0" + line 198, "pan.___", state 122, "sensea?_" + line 202, "pan.___", state 126, "lastpacedpulsev = timer" + line 202, "pan.___", state 127, "avdelay = -(1)" + line 202, "pan.___", state 128, "sensev?_" + line 204, "pan.___", state 131, "lastpacedpulsev = timer" + line 204, "pan.___", state 132, "avdelay = -(1)" + line 204, "pan.___", state 133, "pulsev!1" + line 212, "pan.___", state 150, "-end-" + (33 of 150 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 273, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0 seconds +0.00user 0.01system 0:00.03elapsed 50%CPU (0avgtext+0avgdata 12224maxresident)k +0inputs+8outputs (0major+804minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/LRLURLA_RC.ltl b/verified_pacemaker/LRLURLA_RC.ltl new file mode 100644 index 0000000..04fd7ff --- /dev/null +++ b/verified_pacemaker/LRLURLA_RC.ltl @@ -0,0 +1,114 @@ +#define p lastpacedpulsea <= maxtime +#define q lastpacedpulsea > 0 +#define r lastpacedpulsea >= (sensortime + responsefactor*incrementtime) /* + * Formula As Typed: [] (p && (q -> r)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p && (q -> r))) + * (formalizing violations of the original) + */ + +never { /* !([] (p && (q -> r))) */ +T0_init: + if + :: (((! ((p))) || (! ((r)) && (q) && ((! ((p))) || (! ((r)) && (q)))))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 268) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 922, errors: 0 + 460 states, stored + 1 states, matched + 461 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.049 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.267 actual memory usage for states (unsuccessful compression: 542.77%) + state-vector as stored = 592 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.501 total actual memory usage + +unreached in proctype updatetimers + line 37, "pan.___", state 13, "avdelay = 0" + line 38, "pan.___", state 14, "lastpacedpulsea = 0" + line 42, "pan.___", state 20, "avdelay = (avdelay+100)" + line 47, "pan.___", state 32, "-end-" + (4 of 32 states) +unreached in proctype environment + line 58, "pan.___", state 5, "lastpulse = timer" + line 58, "pan.___", state 6, "avdelay = 0" + line 62, "pan.___", state 12, "avdelay = -(1)" + line 105, "pan.___", state 67, "-end-" + (4 of 67 states) +unreached in proctype sensor + line 117, "pan.___", state 23, "-end-" + (1 of 23 states) +unreached in proctype pacegen + line 137, "pan.___", state 20, "lastpacedpulsea = timer" + line 137, "pan.___", state 21, "avdelay = 0" + line 146, "pan.___", state 35, "lastpacedpulsev = timer" + line 146, "pan.___", state 36, "avdelay = -(1)" + line 146, "pan.___", state 37, "sensev?_" + line 150, "pan.___", state 41, "lastpacedpulsev = timer" + line 150, "pan.___", state 42, "avdelay = -(1)" + line 159, "pan.___", state 56, "lastpacedpulsea = timer" + line 159, "pan.___", state 57, "avdelay = 0" + line 159, "pan.___", state 58, "sensea?_" + line 163, "pan.___", state 62, "lastpacedpulsea = timer" + line 163, "pan.___", state 63, "avdelay = 0" + line 172, "pan.___", state 77, "pulsev!1" + line 172, "pan.___", state 78, "lastpacedpulsev = timer" + line 172, "pan.___", state 79, "avdelay = -(1)" + line 172, "pan.___", state 80, "sensev?_" + line 176, "pan.___", state 84, "lastpacedpulsev = timer" + line 176, "pan.___", state 85, "avdelay = -(1)" + line 185, "pan.___", state 99, "pulsea!1" + line 185, "pan.___", state 100, "lastpacedpulsea = timer" + line 185, "pan.___", state 101, "avdelay = 0" + line 185, "pan.___", state 102, "sensea?_" + line 189, "pan.___", state 106, "lastpacedpulsea = timer" + line 189, "pan.___", state 107, "avdelay = 0" + line 198, "pan.___", state 121, "avdelay = 0" + line 198, "pan.___", state 122, "sensea?_" + line 202, "pan.___", state 126, "lastpacedpulsev = timer" + line 202, "pan.___", state 127, "avdelay = -(1)" + line 202, "pan.___", state 128, "sensev?_" + line 204, "pan.___", state 131, "lastpacedpulsev = timer" + line 204, "pan.___", state 132, "avdelay = -(1)" + line 204, "pan.___", state 133, "pulsev!1" + line 212, "pan.___", state 150, "-end-" + (33 of 150 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 273, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0 seconds +0.00user 0.01system 0:00.03elapsed 50%CPU (0avgtext+0avgdata 12224maxresident)k +0inputs+8outputs (0major+804minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/LRLURLV.ltl b/verified_pacemaker/LRLURLV.ltl new file mode 100644 index 0000000..f2ae6f7 --- /dev/null +++ b/verified_pacemaker/LRLURLV.ltl @@ -0,0 +1,116 @@ +#define p lastpacedpulsev <= maxtime +#define q lastpacedpulsev > 0 +#define r lastpacedpulsev >= mintime + + /* + * Formula As Typed: [] (p && (q -> r)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p && (q -> r))) + * (formalizing violations of the original) + */ + +never { /* !([] (p && (q -> r))) */ +T0_init: + if + :: (((! ((p))) || (! ((r)) && (q) && ((! ((p))) || (! ((r)) && (q)))))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 268) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 922, errors: 0 + 460 states, stored + 1 states, matched + 461 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.049 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.267 actual memory usage for states (unsuccessful compression: 542.77%) + state-vector as stored = 592 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.501 total actual memory usage + +unreached in proctype updatetimers + line 37, "pan.___", state 13, "avdelay = 0" + line 38, "pan.___", state 14, "lastpacedpulsea = 0" + line 42, "pan.___", state 20, "avdelay = (avdelay+100)" + line 47, "pan.___", state 32, "-end-" + (4 of 32 states) +unreached in proctype environment + line 58, "pan.___", state 5, "lastpulse = timer" + line 58, "pan.___", state 6, "avdelay = 0" + line 62, "pan.___", state 12, "avdelay = -(1)" + line 105, "pan.___", state 67, "-end-" + (4 of 67 states) +unreached in proctype sensor + line 117, "pan.___", state 23, "-end-" + (1 of 23 states) +unreached in proctype pacegen + line 137, "pan.___", state 20, "lastpacedpulsea = timer" + line 137, "pan.___", state 21, "avdelay = 0" + line 146, "pan.___", state 35, "lastpacedpulsev = timer" + line 146, "pan.___", state 36, "avdelay = -(1)" + line 146, "pan.___", state 37, "sensev?_" + line 150, "pan.___", state 41, "lastpacedpulsev = timer" + line 150, "pan.___", state 42, "avdelay = -(1)" + line 159, "pan.___", state 56, "lastpacedpulsea = timer" + line 159, "pan.___", state 57, "avdelay = 0" + line 159, "pan.___", state 58, "sensea?_" + line 163, "pan.___", state 62, "lastpacedpulsea = timer" + line 163, "pan.___", state 63, "avdelay = 0" + line 172, "pan.___", state 77, "pulsev!1" + line 172, "pan.___", state 78, "lastpacedpulsev = timer" + line 172, "pan.___", state 79, "avdelay = -(1)" + line 172, "pan.___", state 80, "sensev?_" + line 176, "pan.___", state 84, "lastpacedpulsev = timer" + line 176, "pan.___", state 85, "avdelay = -(1)" + line 185, "pan.___", state 99, "pulsea!1" + line 185, "pan.___", state 100, "lastpacedpulsea = timer" + line 185, "pan.___", state 101, "avdelay = 0" + line 185, "pan.___", state 102, "sensea?_" + line 189, "pan.___", state 106, "lastpacedpulsea = timer" + line 189, "pan.___", state 107, "avdelay = 0" + line 198, "pan.___", state 121, "avdelay = 0" + line 198, "pan.___", state 122, "sensea?_" + line 202, "pan.___", state 126, "lastpacedpulsev = timer" + line 202, "pan.___", state 127, "avdelay = -(1)" + line 202, "pan.___", state 128, "sensev?_" + line 204, "pan.___", state 131, "lastpacedpulsev = timer" + line 204, "pan.___", state 132, "avdelay = -(1)" + line 204, "pan.___", state 133, "pulsev!1" + line 212, "pan.___", state 150, "-end-" + (33 of 150 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 273, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0 seconds +0.00user 0.01system 0:00.03elapsed 50%CPU (0avgtext+0avgdata 12224maxresident)k +0inputs+8outputs (0major+804minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/LRLURLV_R.ltl b/verified_pacemaker/LRLURLV_R.ltl new file mode 100644 index 0000000..16050c8 --- /dev/null +++ b/verified_pacemaker/LRLURLV_R.ltl @@ -0,0 +1,114 @@ +#define p lastpacedpulsev <= maxtime +#define q lastpacedpulsev > 0 +#define r lastpacedpulsev >= sensortime /* + * Formula As Typed: [] (p && (q -> r)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p && (q -> r))) + * (formalizing violations of the original) + */ + +never { /* !([] (p && (q -> r))) */ +T0_init: + if + :: (((! ((p))) || (! ((r)) && (q) && ((! ((p))) || (! ((r)) && (q)))))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 268) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 922, errors: 0 + 460 states, stored + 1 states, matched + 461 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.049 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.267 actual memory usage for states (unsuccessful compression: 542.77%) + state-vector as stored = 592 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.501 total actual memory usage + +unreached in proctype updatetimers + line 37, "pan.___", state 13, "avdelay = 0" + line 38, "pan.___", state 14, "lastpacedpulsea = 0" + line 42, "pan.___", state 20, "avdelay = (avdelay+100)" + line 47, "pan.___", state 32, "-end-" + (4 of 32 states) +unreached in proctype environment + line 58, "pan.___", state 5, "lastpulse = timer" + line 58, "pan.___", state 6, "avdelay = 0" + line 62, "pan.___", state 12, "avdelay = -(1)" + line 105, "pan.___", state 67, "-end-" + (4 of 67 states) +unreached in proctype sensor + line 117, "pan.___", state 23, "-end-" + (1 of 23 states) +unreached in proctype pacegen + line 137, "pan.___", state 20, "lastpacedpulsea = timer" + line 137, "pan.___", state 21, "avdelay = 0" + line 146, "pan.___", state 35, "lastpacedpulsev = timer" + line 146, "pan.___", state 36, "avdelay = -(1)" + line 146, "pan.___", state 37, "sensev?_" + line 150, "pan.___", state 41, "lastpacedpulsev = timer" + line 150, "pan.___", state 42, "avdelay = -(1)" + line 159, "pan.___", state 56, "lastpacedpulsea = timer" + line 159, "pan.___", state 57, "avdelay = 0" + line 159, "pan.___", state 58, "sensea?_" + line 163, "pan.___", state 62, "lastpacedpulsea = timer" + line 163, "pan.___", state 63, "avdelay = 0" + line 172, "pan.___", state 77, "pulsev!1" + line 172, "pan.___", state 78, "lastpacedpulsev = timer" + line 172, "pan.___", state 79, "avdelay = -(1)" + line 172, "pan.___", state 80, "sensev?_" + line 176, "pan.___", state 84, "lastpacedpulsev = timer" + line 176, "pan.___", state 85, "avdelay = -(1)" + line 185, "pan.___", state 99, "pulsea!1" + line 185, "pan.___", state 100, "lastpacedpulsea = timer" + line 185, "pan.___", state 101, "avdelay = 0" + line 185, "pan.___", state 102, "sensea?_" + line 189, "pan.___", state 106, "lastpacedpulsea = timer" + line 189, "pan.___", state 107, "avdelay = 0" + line 198, "pan.___", state 121, "avdelay = 0" + line 198, "pan.___", state 122, "sensea?_" + line 202, "pan.___", state 126, "lastpacedpulsev = timer" + line 202, "pan.___", state 127, "avdelay = -(1)" + line 202, "pan.___", state 128, "sensev?_" + line 204, "pan.___", state 131, "lastpacedpulsev = timer" + line 204, "pan.___", state 132, "avdelay = -(1)" + line 204, "pan.___", state 133, "pulsev!1" + line 212, "pan.___", state 150, "-end-" + (33 of 150 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 273, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0 seconds +0.00user 0.01system 0:00.03elapsed 50%CPU (0avgtext+0avgdata 12224maxresident)k +0inputs+8outputs (0major+804minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/LRLURLV_RC.ltl b/verified_pacemaker/LRLURLV_RC.ltl new file mode 100644 index 0000000..3aa67ba --- /dev/null +++ b/verified_pacemaker/LRLURLV_RC.ltl @@ -0,0 +1,114 @@ +#define p lastpacedpulsev <= maxtime +#define q lastpacedpulsev > 0 +#define r lastpacedpulsev >= (sensortime + responsefactor*incrementtime) /* + * Formula As Typed: [] (p && (q -> r)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p && (q -> r))) + * (formalizing violations of the original) + */ + +never { /* !([] (p && (q -> r))) */ +T0_init: + if + :: (((! ((p))) || (! ((r)) && (q) && ((! ((p))) || (! ((r)) && (q)))))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 268) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 922, errors: 0 + 460 states, stored + 1 states, matched + 461 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.049 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.267 actual memory usage for states (unsuccessful compression: 542.77%) + state-vector as stored = 592 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.501 total actual memory usage + +unreached in proctype updatetimers + line 37, "pan.___", state 13, "avdelay = 0" + line 38, "pan.___", state 14, "lastpacedpulsea = 0" + line 42, "pan.___", state 20, "avdelay = (avdelay+100)" + line 47, "pan.___", state 32, "-end-" + (4 of 32 states) +unreached in proctype environment + line 58, "pan.___", state 5, "lastpulse = timer" + line 58, "pan.___", state 6, "avdelay = 0" + line 62, "pan.___", state 12, "avdelay = -(1)" + line 105, "pan.___", state 67, "-end-" + (4 of 67 states) +unreached in proctype sensor + line 117, "pan.___", state 23, "-end-" + (1 of 23 states) +unreached in proctype pacegen + line 137, "pan.___", state 20, "lastpacedpulsea = timer" + line 137, "pan.___", state 21, "avdelay = 0" + line 146, "pan.___", state 35, "lastpacedpulsev = timer" + line 146, "pan.___", state 36, "avdelay = -(1)" + line 146, "pan.___", state 37, "sensev?_" + line 150, "pan.___", state 41, "lastpacedpulsev = timer" + line 150, "pan.___", state 42, "avdelay = -(1)" + line 159, "pan.___", state 56, "lastpacedpulsea = timer" + line 159, "pan.___", state 57, "avdelay = 0" + line 159, "pan.___", state 58, "sensea?_" + line 163, "pan.___", state 62, "lastpacedpulsea = timer" + line 163, "pan.___", state 63, "avdelay = 0" + line 172, "pan.___", state 77, "pulsev!1" + line 172, "pan.___", state 78, "lastpacedpulsev = timer" + line 172, "pan.___", state 79, "avdelay = -(1)" + line 172, "pan.___", state 80, "sensev?_" + line 176, "pan.___", state 84, "lastpacedpulsev = timer" + line 176, "pan.___", state 85, "avdelay = -(1)" + line 185, "pan.___", state 99, "pulsea!1" + line 185, "pan.___", state 100, "lastpacedpulsea = timer" + line 185, "pan.___", state 101, "avdelay = 0" + line 185, "pan.___", state 102, "sensea?_" + line 189, "pan.___", state 106, "lastpacedpulsea = timer" + line 189, "pan.___", state 107, "avdelay = 0" + line 198, "pan.___", state 121, "avdelay = 0" + line 198, "pan.___", state 122, "sensea?_" + line 202, "pan.___", state 126, "lastpacedpulsev = timer" + line 202, "pan.___", state 127, "avdelay = -(1)" + line 202, "pan.___", state 128, "sensev?_" + line 204, "pan.___", state 131, "lastpacedpulsev = timer" + line 204, "pan.___", state 132, "avdelay = -(1)" + line 204, "pan.___", state 133, "pulsev!1" + line 212, "pan.___", state 150, "-end-" + (33 of 150 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 273, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0 seconds +0.00user 0.01system 0:00.03elapsed 50%CPU (0avgtext+0avgdata 12224maxresident)k +0inputs+8outputs (0major+804minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/PVARP.ltl b/verified_pacemaker/PVARP.ltl new file mode 100644 index 0000000..d645eee --- /dev/null +++ b/verified_pacemaker/PVARP.ltl @@ -0,0 +1,146 @@ +#define p lastpacedpulsea > lastsenseda +#define r (lastpacedpulsea - lastsenseda) > pvarp +#define q lastpacedpulsev > lastsensedv +#define s (lastpacedpulsev - lastsensedv) > pvarp + + /* + * Formula As Typed: [] ((p && q) -> (r && s)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] ((p && q) -> (r && s))) + * (formalizing violations of the original) + */ + +never { /* !([] ((p && q) -> (r && s))) */ +T0_init: + if + :: (((! ((r)) && (p) && (q)) || (! ((s)) && (p) && (q)))) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 369) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 124 byte, depth reached 23295, errors: 0 + 18067 states, stored + 397 states, matched + 18464 transitions (= stored+matched) + 4 atomic steps +hash conflicts: 8 (resolved) + +Stats on memory usage (in Megabytes): + 2.412 equivalent memory usage for states (stored*(State-vector + overhead)) + 2.108 actual memory usage for states (compression: 87.41%) + state-vector as stored = 106 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 3.052 memory used for DFS stack (-m100000) + 7.103 total actual memory usage + +unreached in proctype updatetimers + line 39, "pan.___", state 4, "timer = 0" + line 40, "pan.___", state 5, "avdelay = -(1)" + line 40, "pan.___", state 6, "lastpulse = 0" + line 44, "pan.___", state 12, "timer = 0" + line 45, "pan.___", state 13, "avdelay = -(1)" + line 45, "pan.___", state 14, "lastpacedpulsev = 0" + line 46, "pan.___", state 15, "lastpulse = 0" + line 65, "pan.___", state 47, "-end-" + (8 of 47 states) +unreached in proctype environment + line 76, "pan.___", state 5, "lastpulse = timer" + line 76, "pan.___", state 6, "avdelay = 0" + line 76, "pan.___", state 8, "lastpulse = timer" + line 76, "pan.___", state 9, "avdelay = 0" + line 76, "pan.___", state 10, "pula = 1" + line 76, "pan.___", state 10, "timer = 0" + line 82, "pan.___", state 18, "avdelay = -(1)" + line 82, "pan.___", state 20, "avdelay = -(1)" + line 82, "pan.___", state 21, "pulv = 1" + line 82, "pan.___", state 21, "timer = 0" + line 93, "pan.___", state 34, "lastpulse = timer" + line 93, "pan.___", state 35, "avdelay = 0" + line 93, "pan.___", state 36, "pula = 1" + line 97, "pan.___", state 40, "avdelay = -(1)" + line 97, "pan.___", state 41, "timer = 0" + line 121, "pan.___", state 78, "-end-" + (14 of 78 states) +unreached in proctype sensor + line 139, "pan.___", state 41, "-end-" + (1 of 41 states) +unreached in proctype pacegen + line 153, "pan.___", state 14, "pulv = 1" + line 153, "pan.___", state 15, "lastpacedpulsev = timer" + line 153, "pan.___", state 16, "avdelay = -(1)" + line 167, "pan.___", state 39, "pula = 1" + line 167, "pan.___", state 40, "lastpacedpulsea = timer" + line 167, "pan.___", state 41, "avdelay = 0" + line 175, "pan.___", state 54, "lastpacedpulsev = timer" + line 175, "pan.___", state 55, "avdelay = -(1)" + line 182, "pan.___", state 63, "pulv = 1" + line 182, "pan.___", state 64, "lastpacedpulsev = timer" + line 182, "pan.___", state 65, "avdelay = -(1)" + line 184, "pan.___", state 71, "pulv = 1" + line 184, "pan.___", state 72, "lastpacedpulsev = timer" + line 184, "pan.___", state 73, "avdelay = -(1)" + line 180, "pan.___", state 74, "(((mode==VVIR)||(mode==DDIR)))" + line 180, "pan.___", state 74, "else" + line 192, "pan.___", state 86, "lastpacedpulsea = timer" + line 192, "pan.___", state 87, "avdelay = 0" + line 199, "pan.___", state 95, "pula = 1" + line 199, "pan.___", state 96, "lastpacedpulsea = timer" + line 199, "pan.___", state 97, "avdelay = 0" + line 201, "pan.___", state 103, "pula = 1" + line 201, "pan.___", state 104, "lastpacedpulsea = timer" + line 201, "pan.___", state 105, "avdelay = 0" + line 197, "pan.___", state 106, "(((mode==AAIR)||(mode==DDIR)))" + line 197, "pan.___", state 106, "else" + line 209, "pan.___", state 118, "pulv = 1" + line 209, "pan.___", state 119, "lastpacedpulsev = timer" + line 209, "pan.___", state 120, "avdelay = -(1)" + line 214, "pan.___", state 127, "lastpacedpulsev = timer" + line 214, "pan.___", state 128, "avdelay = -(1)" + line 214, "pan.___", state 129, "pulv = 1" + line 222, "pan.___", state 141, "pula = 1" + line 222, "pan.___", state 142, "lastpacedpulsea = timer" + line 222, "pan.___", state 143, "avdelay = 0" + line 227, "pan.___", state 150, "lastpacedpulsea = timer" + line 227, "pan.___", state 151, "avdelay = 0" + line 227, "pan.___", state 152, "pula = 1" + line 245, "pan.___", state 181, "pulv = 1" + line 245, "pan.___", state 182, "lastpacedpulsev = timer" + line 245, "pan.___", state 183, "avdelay = -(1)" + line 252, "pan.___", state 199, "-end-" + (40 of 199 states) +unreached in proctype accelerometer + line 284, "pan.___", state 59, "-end-" + (1 of 59 states) +unreached in proctype :init: + (0 of 7 states) +unreached in proctype :never: + line 374, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0.312 seconds +pan: rate 57907.051 states/second +pan: avg transition delay 1.6898e-005 usec + +#endif diff --git a/verified_pacemaker/README.txt b/verified_pacemaker/README.txt new file mode 100644 index 0000000..1b7e459 --- /dev/null +++ b/verified_pacemaker/README.txt @@ -0,0 +1,176 @@ +List of Files Containted - + +AAI.ltl +AAI_H.ltl +AAT.ltl +ARP.ltl +AVD.ltl +Distributed_AVD.ltl +LRLURLA.ltl +LRLURLA_R.ltl +LRLURLA_RC.ltl +LRLURLV.ltl +LRLURLV_R.ltl +LRLURLV_RC.ltl +pacemaker.c (C Implementation Code) +pacemaker.h +pacemaker_concurrent.pml +pacemaker_C_Code.pml +pacemaker_distributed.pml +pacemaker_sequential.pml +PVARP.ltl +README.txt (this file) +VRP.ltl +VVI.ltl +VVI_H.ltl +VVT.ltl +XDD.ltl +XDD_H.ltl + + +=================== +Models of Pacemaker +=================== + +------------------------------------- +Sequential - pacemaker_sequential.pml +------------------------------------- + +Change the default max depth from 10000 to 100000 + +- Default Configuration is + + mode = nondet + behave = nondet + hysteresis = 1 + + Check for invalid end state - Deadlock freeness + +- TO verify all the generic properties, in the init process set + + mode = nondet + behave = nondet + hysteresis = 0 + + use LTL property manager to load and check + LRLURLA, LRLURLV, AVD, ARP, VRP and PVARP + + +- To verify Inhibiting properties, in the init process set + + mode = VVI or AAI + behave = nondet + hysteresis = 0 + + use LTL property manager to load and check + AAI and VVI + +- To verify Triggering properties, in the init process set + + mode = VVT or AAT + behave = nondet + hysteresis = 0 + + use LTL property manager to load and check + AAT and VVT + +- To verify Tracking properties, in the init process set + + mode = VDD or DDD + behave = nondet + hysteresis = 0 + + use LTL property manager to load and check + XDD + +- To verify Rate Control properties, in the init process set + + mode = VOOR or AOOR or DOOR or VVIR or AAIR or DDIR or VDDR or DDDR + behave = nondet + hysteresis = 0 + + use LTL property manager to load and check + LRLURLA_R, LRLURLA_RC, LRLURLV_R and LRLURLV_RC + +- To verify Hysteresis properties, in the init process set + + mode = nondet + behave = nondet + hysteresis = 1 + + use LTL property manager to load and check + AAI_H, VVI_H and XDD_H + +------------------------------------- +Concurrent - pacemaker_concurrent.pml +------------------------------------- + +Change the max memory used by SPIN to 2000 MB + + +- Default Configuration is + + mode = nondet + behave = nondet + + Check for invalid end state - Deadlock freeness + +- TO verify all the generic properties, in the init process set + + mode = nondet + behave = nondet + + + use LTL property manager to load and check + LRLURLA, LRLURLV and AVD + +--------------------------------------- +Distributed - pacemaker_distributed.pml +--------------------------------------- + +Choose to use memory compression in SPIN + + +- Default Configuration is + + mode = nondet + behave = nondet + + Check for invalid end state - Deadlock freeness + +- TO verify all the generic properties, in the init process set + + mode = nondet + behave = nondet + + + use LTL property manager to load and check + LRLURLA, LRLURLV, AVD and Distributed_AVD + +------------------------------------------------------ +Embedded C Code - pacemaker_C_Code.pml and pacemaker.h +------------------------------------------------------ + +- Default Configuration is + + PROMELA init() + mode = nondet + behave = nondet + + c_code config + mode = DDDR + hysteresis = 1 + + Check for invalid end state - Deadlock freeness + +- TO verify all the LTL properties, in the c_code part of Pace Generator process set + + mode = XXXX (Any given mode) + + use LTL property manager to load and check properties as in Sequential Model + +------------------------------ +C Implementation - pacemaker.c +------------------------------ + +A sequential implementaion of the pacemaker in C that can be compiled and run with gcc. \ No newline at end of file diff --git a/verified_pacemaker/Testing_C_Code_Branch_Coverage.pml.ltl b/verified_pacemaker/Testing_C_Code_Branch_Coverage.pml.ltl new file mode 100644 index 0000000..7b04c2d --- /dev/null +++ b/verified_pacemaker/Testing_C_Code_Branch_Coverage.pml.ltl @@ -0,0 +1,70 @@ +#define p imode == 0 +#define q imode == 1 +#define r imode == 2 +#define s imode == 3 +#define t imode == 4 +#define u imode == 5 +#define v imode == 8 +#define w imode == 6 +#define x endstate == 1 + + /* + * Formula As Typed: [] ((p || q || r || s || t || u || v || w) -><> x) + * The Never Claim Below Corresponds + * To The Negated Formula !([] ((p || q || r || s || t || u || v || w) -><> x)) + * (formalizing violations of the original) + */ + +never { /* !([] ((p || q || r || s || t || u || v || w) -><> x)) */ +T0_init: + if + :: (((! ((x)) && (p)) || (((! ((x)) && (q)) || (((! ((x)) && (r)) || (((! ((x)) && (s)) || (((! ((x)) && (t)) || (((! ((x)) && (u)) || (((! ((x)) && (v)) || (! ((x)) && (w)))))))))))))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (! ((x))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 343) +depth 2: Claim reached state 9 (line 348) +depth 112: Claim reached state 9 (line 348) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 148 byte, depth reached 6059, errors: 0 + 3253 states, stored (3334 visited) + 385 states, matched + 3719 transitions (= visited+matched) + 16 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.509 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.652 actual memory usage for states (unsuccessful compression: 128.20%) + state-vector as stored = 194 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.891 total actual memory usage + + +pan: elapsed time 0.016 seconds +pan: rate 208375 states/second +pan: avg transition delay 4.3022e-006 usec + +#endif diff --git a/verified_pacemaker/VRP.ltl b/verified_pacemaker/VRP.ltl new file mode 100644 index 0000000..0d4ef99 --- /dev/null +++ b/verified_pacemaker/VRP.ltl @@ -0,0 +1,148 @@ +#define p lastpacedpulsev > lastsensedv +#define r (lastpacedpulsev - lastsensedv) > vrp + + /* + * Formula As Typed: [] (p -> r) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> r)) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> r)) */ +T0_init: + if + :: (! ((r)) && (p)) -> goto accept_all + :: (1) -> goto T0_init + fi; +accept_all: + skip +} + +#ifdef NOTES +Use Load to open a file or a template. + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 297) +pan:1: claim violated! (at depth 1452) +pan: wrote pan_in.trail + +(Spin Version 5.2.5 -- 17 April 2010) +Warning: Search not completed + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 104 byte, depth reached 1452, errors: 1 + 725 states, stored + 0 states, matched + 725 transitions (= stored+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.083 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.262 actual memory usage for states (unsuccessful compression: 316.33%) + state-vector as stored = 364 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.501 total actual memory usage + +unreached in proctype updatetimers + line 35, "pan.___", state 4, "timer = 0" + line 36, "pan.___", state 5, "avdelay = -(1)" + line 36, "pan.___", state 6, "lastpulse = 0" + line 40, "pan.___", state 12, "timer = 0" + line 41, "pan.___", state 13, "avdelay = -(1)" + line 41, "pan.___", state 14, "lastpacedpulsev = 0" + line 42, "pan.___", state 15, "lastpulse = 0" + line 51, "pan.___", state 28, "avdelay = 0" + line 52, "pan.___", state 29, "lastpacedpulsea = 0" + line 56, "pan.___", state 35, "avdelay = (avdelay+50)" + line 61, "pan.___", state 47, "-end-" + (11 of 47 states) +unreached in proctype environment + line 72, "pan.___", state 5, "lastpulse = timer" + line 72, "pan.___", state 6, "avdelay = 0" + line 72, "pan.___", state 8, "lastpulse = timer" + line 72, "pan.___", state 9, "avdelay = 0" + line 72, "pan.___", state 10, "pula = 1" + line 72, "pan.___", state 10, "timer = 0" + line 78, "pan.___", state 18, "avdelay = -(1)" + line 78, "pan.___", state 20, "avdelay = -(1)" + line 78, "pan.___", state 21, "pulv = 1" + line 78, "pan.___", state 21, "timer = 0" + line 89, "pan.___", state 34, "lastpulse = timer" + line 89, "pan.___", state 35, "avdelay = 0" + line 89, "pan.___", state 36, "pula = 1" + line 93, "pan.___", state 40, "avdelay = -(1)" + line 93, "pan.___", state 41, "timer = 0" + line 105, "pan.___", state 54, "lastpulse = timer" + line 105, "pan.___", state 55, "avdelay = 0" + line 105, "pan.___", state 56, "timer = 0" + line 109, "pan.___", state 60, "avdelay = -(1)" + line 109, "pan.___", state 61, "timer = 0" + line 117, "pan.___", state 78, "-end-" + (19 of 78 states) +unreached in proctype sensor + line 123, "pan.___", state 3, "sena = 0" + line 123, "pan.___", state 4, "pula = 0" + line 126, "pan.___", state 10, "sena = 1" + line 126, "pan.___", state 11, "pula = 0" + line 126, "pan.___", state 12, "lastsenseda = timer" + line 128, "pan.___", state 19, "senv = 0" + line 128, "pan.___", state 20, "pulv = 0" + line 128, "pan.___", state 21, "lastsensedv = 0" + line 135, "pan.___", state 42, "-end-" + (9 of 42 states) +unreached in proctype pacegen + line 145, "pan.___", state 5, "lastpacedpulsev = timer" + line 145, "pan.___", state 6, "avdelay = -(1)" + line 145, "pan.___", state 7, "pulv = 1" + line 155, "pan.___", state 20, "lastpacedpulsea = timer" + line 155, "pan.___", state 21, "avdelay = 0" + line 155, "pan.___", state 22, "pula = 1" + line 176, "pan.___", state 56, "lastpacedpulsea = timer" + line 176, "pan.___", state 57, "avdelay = 0" + line 181, "pan.___", state 64, "lastpacedpulsea = timer" + line 181, "pan.___", state 65, "avdelay = 0" + line 181, "pan.___", state 66, "pula = 1" + line 189, "pan.___", state 78, "pulv = 1" + line 189, "pan.___", state 79, "lastpacedpulsev = timer" + line 189, "pan.___", state 80, "avdelay = -(1)" + line 194, "pan.___", state 87, "lastpacedpulsev = timer" + line 194, "pan.___", state 88, "avdelay = -(1)" + line 194, "pan.___", state 89, "pulv = 1" + line 202, "pan.___", state 101, "pula = 1" + line 202, "pan.___", state 102, "lastpacedpulsea = timer" + line 202, "pan.___", state 103, "avdelay = 0" + line 207, "pan.___", state 110, "lastpacedpulsea = timer" + line 207, "pan.___", state 111, "avdelay = 0" + line 207, "pan.___", state 112, "pula = 1" + line 215, "pan.___", state 124, "avdelay = 0" + line 218, "pan.___", state 130, "avdelay = -(1)" + line 225, "pan.___", state 141, "pulv = 1" + line 225, "pan.___", state 142, "lastpacedpulsev = timer" + line 225, "pan.___", state 143, "avdelay = -(1)" + line 232, "pan.___", state 159, "-end-" + (29 of 159 states) +unreached in proctype :init: + line 243, "pan.___", state 6, "-end-" + (1 of 6 states) +unreached in proctype :never: + line 302, "pan.___", state 8, "-end-" + (1 of 8 states) + +pan: elapsed time 0.07 seconds +pan: rate 10357.143 states/second +pan: avg transition delay 9.6552e-05 usec +0.00user 0.03system 0:00.14elapsed 22%CPU (0avgtext+0avgdata 12400maxresident)k +0inputs+48outputs (0major+816minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/VVI.ltl b/verified_pacemaker/VVI.ltl new file mode 100644 index 0000000..a4068ad --- /dev/null +++ b/verified_pacemaker/VVI.ltl @@ -0,0 +1,148 @@ +#define p senv == 1 +#define q pulv == 0 +#define r avdelay == -1 +#define s lastpacedpulsev == timer + + /* + * Formula As Typed: [] (p -> <> (q && r && s)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> <> (q && r && s))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> <> (q && r && s))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (! ((s)) && (p)))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (! ((s))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 291) +depth 1237: Claim reached state 9 (line 296) +depth 1259: Claim reached state 9 (line 296) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 3078, errors: 0 + 2371 states, stored (3245 visited) + 986 states, matched + 4231 transitions (= visited+matched) + 3 atomic steps +hash conflicts: 4 (resolved) + +Stats on memory usage (in Megabytes): + 0.253 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.361 actual memory usage for states (unsuccessful compression: 142.66%) + state-vector as stored = 144 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.598 total actual memory usage + +unreached in proctype updatetimers + line 31, "pan.___", state 4, "timer = 0" + line 32, "pan.___", state 5, "avdelay = -(1)" + line 32, "pan.___", state 6, "lastpulse = 0" + line 36, "pan.___", state 12, "timer = 0" + line 37, "pan.___", state 13, "avdelay = -(1)" + line 37, "pan.___", state 14, "lastpacedpulsev = 0" + line 38, "pan.___", state 15, "lastpulse = 0" + line 47, "pan.___", state 28, "avdelay = 0" + line 48, "pan.___", state 29, "lastpacedpulsea = 0" + line 57, "pan.___", state 47, "-end-" + (10 of 47 states) +unreached in proctype environment + line 68, "pan.___", state 5, "lastpulse = timer" + line 68, "pan.___", state 6, "avdelay = 0" + line 68, "pan.___", state 8, "lastpulse = timer" + line 68, "pan.___", state 9, "avdelay = 0" + line 68, "pan.___", state 10, "pula = 1" + line 68, "pan.___", state 10, "timer = 0" + line 71, "pan.___", state 14, "avdelay = -(1)" + line 71, "pan.___", state 16, "avdelay = -(1)" + line 71, "pan.___", state 17, "pulv = 1" + line 71, "pan.___", state 17, "timer = 0" + line 82, "pan.___", state 30, "lastpulse = timer" + line 82, "pan.___", state 31, "avdelay = 0" + line 82, "pan.___", state 32, "pula = 1" + line 86, "pan.___", state 36, "avdelay = -(1)" + line 86, "pan.___", state 37, "timer = 0" + line 111, "pan.___", state 73, "-end-" + (14 of 73 states) +unreached in proctype sensor + line 117, "pan.___", state 3, "sena = 1" + line 117, "pan.___", state 4, "pula = 0" + line 123, "pan.___", state 23, "-end-" + (3 of 23 states) +unreached in proctype pacegen + line 133, "pan.___", state 5, "lastpacedpulsev = timer" + line 133, "pan.___", state 6, "avdelay = -(1)" + line 133, "pan.___", state 7, "pulv = 1" + line 143, "pan.___", state 20, "lastpacedpulsea = timer" + line 143, "pan.___", state 21, "avdelay = 0" + line 143, "pan.___", state 22, "pula = 1" + line 152, "pan.___", state 34, "pulv = 1" + line 152, "pan.___", state 35, "lastpacedpulsev = timer" + line 152, "pan.___", state 36, "avdelay = -(1)" + line 173, "pan.___", state 69, "lastpacedpulsea = timer" + line 173, "pan.___", state 70, "avdelay = 0" + line 178, "pan.___", state 77, "lastpacedpulsea = timer" + line 178, "pan.___", state 78, "avdelay = 0" + line 178, "pan.___", state 79, "pula = 1" + line 186, "pan.___", state 91, "pulv = 1" + line 186, "pan.___", state 92, "lastpacedpulsev = timer" + line 186, "pan.___", state 93, "avdelay = -(1)" + line 191, "pan.___", state 100, "lastpacedpulsev = timer" + line 191, "pan.___", state 101, "avdelay = -(1)" + line 191, "pan.___", state 102, "pulv = 1" + line 199, "pan.___", state 114, "pulsea!1" + line 199, "pan.___", state 115, "lastpacedpulsea = timer" + line 199, "pan.___", state 116, "avdelay = 0" + line 199, "pan.___", state 117, "sensea?_" + line 203, "pan.___", state 121, "lastpacedpulsea = timer" + line 203, "pan.___", state 122, "avdelay = 0" + line 212, "pan.___", state 136, "avdelay = 0" + line 212, "pan.___", state 137, "sensea?_" + line 216, "pan.___", state 141, "lastpacedpulsev = timer" + line 216, "pan.___", state 142, "avdelay = -(1)" + line 216, "pan.___", state 143, "sensev?_" + line 218, "pan.___", state 146, "lastpacedpulsev = timer" + line 218, "pan.___", state 147, "avdelay = -(1)" + line 218, "pan.___", state 148, "pulsev!1" + line 226, "pan.___", state 165, "-end-" + (35 of 165 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 298, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.03 seconds +pan: rate 108166.67 states/second +pan: avg transition delay 7.0905e-06 usec +0.00user 0.01system 0:00.04elapsed 40%CPU (0avgtext+0avgdata 12880maxresident)k +0inputs+16outputs (0major+845minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/VVI_H.ltl b/verified_pacemaker/VVI_H.ltl new file mode 100644 index 0000000..1a257cf --- /dev/null +++ b/verified_pacemaker/VVI_H.ltl @@ -0,0 +1,159 @@ +#define p senv == 1 +#define q pulv == 0 +#define r avdelay == -1 +#define s lastpacedpulsev == timer +#define t responsefactor == 10 + + + /* + * Formula As Typed: [] (p -> <> (q && r && s && t)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> <> (q && r && s && t))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> <> (q && r && s && t))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (((! ((s)) && (p)) || (! ((t)) && (p)))))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (((! ((s))) || (! ((t))))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 385) +depth 1664: Claim reached state 9 (line 390) +depth 1726: Claim reached state 9 (line 390) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 116 byte, depth reached 12407, errors: 0 + 31876 states, stored (46543 visited) + 17465 states, matched + 64008 transitions (= visited+matched) + 4 atomic steps +hash conflicts: 375 (resolved) + +Stats on memory usage (in Megabytes): + 4.013 equivalent memory usage for states (stored*(State-vector + overhead)) + 3.377 actual memory usage for states (compression: 84.17%) + state-vector as stored = 95 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 3.052 memory used for DFS stack (-m100000) + 8.372 total actual memory usage + +unreached in proctype updatetimers + line 45, "pan.___", state 12, "timer = 0" + line 46, "pan.___", state 13, "avdelay = -(1)" + line 46, "pan.___", state 14, "lastpacedpulsev = 0" + line 47, "pan.___", state 15, "lastpulse = 0" + line 51, "pan.___", state 21, "avdelay = -(1)" + line 52, "pan.___", state 22, "lastpacedpulsev = 0" + line 66, "pan.___", state 47, "-end-" + (7 of 47 states) +unreached in proctype environment + line 94, "pan.___", state 34, "lastpulse = timer" + line 94, "pan.___", state 35, "avdelay = 0" + line 94, "pan.___", state 36, "pula = 1" + line 98, "pan.___", state 40, "avdelay = -(1)" + line 98, "pan.___", state 41, "timer = 0" + line 110, "pan.___", state 54, "lastpulse = timer" + line 110, "pan.___", state 55, "avdelay = 0" + line 110, "pan.___", state 56, "timer = 0" + line 114, "pan.___", state 60, "avdelay = -(1)" + line 114, "pan.___", state 61, "timer = 0" + line 122, "pan.___", state 78, "-end-" + (11 of 78 states) +unreached in proctype sensor + line 133, "pan.___", state 19, "senv = 0" + line 133, "pan.___", state 20, "pulv = 0" + line 140, "pan.___", state 41, "-end-" + (3 of 41 states) +unreached in proctype pacegen + line 152, "pan.___", state 6, "pulv = 1" + line 152, "pan.___", state 7, "lastpacedpulsev = timer" + line 152, "pan.___", state 8, "avdelay = -(1)" + line 154, "pan.___", state 14, "pulv = 1" + line 154, "pan.___", state 15, "lastpacedpulsev = timer" + line 154, "pan.___", state 16, "avdelay = -(1)" + line 150, "pan.___", state 17, "(((((mode==VOOR)||(mode==DOOR))||(mode==DDDR))||(mode==VDDR)))" + line 150, "pan.___", state 17, "else" + line 166, "pan.___", state 31, "pula = 1" + line 166, "pan.___", state 32, "lastpacedpulsea = timer" + line 166, "pan.___", state 33, "avdelay = 0" + line 168, "pan.___", state 39, "pula = 1" + line 168, "pan.___", state 40, "lastpacedpulsea = timer" + line 168, "pan.___", state 41, "avdelay = 0" + line 164, "pan.___", state 42, "((((mode==AOOR)||(mode==DOOR))||(mode==DDDR)))" + line 164, "pan.___", state 42, "else" + line 176, "pan.___", state 54, "lastpacedpulsev = timer" + line 176, "pan.___", state 55, "avdelay = -(1)" + line 177, "pan.___", state 57, "responsefactor = 10" + line 186, "pan.___", state 69, "pulv = 1" + line 186, "pan.___", state 70, "lastpacedpulsev = timer" + line 186, "pan.___", state 71, "avdelay = -(1)" + line 188, "pan.___", state 77, "pulv = 1" + line 188, "pan.___", state 78, "lastpacedpulsev = timer" + line 188, "pan.___", state 79, "avdelay = -(1)" + line 184, "pan.___", state 80, "(((mode==VVIR)||(mode==DDIR)))" + line 184, "pan.___", state 80, "else" + line 206, "pan.___", state 107, "pula = 1" + line 206, "pan.___", state 108, "lastpacedpulsea = timer" + line 206, "pan.___", state 109, "avdelay = 0" + line 216, "pan.___", state 130, "pulv = 1" + line 216, "pan.___", state 131, "lastpacedpulsev = timer" + line 216, "pan.___", state 132, "avdelay = -(1)" + line 221, "pan.___", state 139, "lastpacedpulsev = timer" + line 221, "pan.___", state 140, "avdelay = -(1)" + line 221, "pan.___", state 141, "pulv = 1" + line 229, "pan.___", state 153, "pula = 1" + line 229, "pan.___", state 154, "lastpacedpulsea = timer" + line 229, "pan.___", state 155, "avdelay = 0" + line 234, "pan.___", state 162, "lastpacedpulsea = timer" + line 234, "pan.___", state 163, "avdelay = 0" + line 234, "pan.___", state 164, "pula = 1" + line 242, "pan.___", state 176, "avdelay = 0" + line 243, "pan.___", state 178, "responsefactor = 10" + line 248, "pan.___", state 188, "avdelay = -(1)" + line 255, "pan.___", state 199, "pulv = 1" + line 255, "pan.___", state 200, "lastpacedpulsev = timer" + line 255, "pan.___", state 201, "avdelay = -(1)" + line 262, "pan.___", state 217, "-end-" + (46 of 217 states) +unreached in proctype accelerometer + line 294, "pan.___", state 59, "-end-" + (1 of 59 states) +unreached in proctype :init: + (0 of 8 states) +unreached in proctype :never: + line 392, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.783 seconds +pan: rate 59441.89 states/second +pan: avg transition delay 1.2233e-005 usec + +#endif diff --git a/verified_pacemaker/VVT.ltl b/verified_pacemaker/VVT.ltl new file mode 100644 index 0000000..13c9050 --- /dev/null +++ b/verified_pacemaker/VVT.ltl @@ -0,0 +1,148 @@ +#define p senv == 1 +#define q pulv == 1 +#define r avdelay == -1 +#define s lastpacedpulsev == timer + + /* + * Formula As Typed: [] (p -> <> (q && r && s)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -> <> (q && r && s))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -> <> (q && r && s))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (! ((s)) && (p)))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (! ((s))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 291) +depth 1237: Claim reached state 9 (line 296) +depth 1269: Claim reached state 9 (line 296) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 3176, errors: 0 + 2368 states, stored (3150 visited) + 1511 states, matched + 4661 transitions (= visited+matched) + 3 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.253 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.361 actual memory usage for states (unsuccessful compression: 142.84%) + state-vector as stored = 144 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.598 total actual memory usage + +unreached in proctype updatetimers + line 31, "pan.___", state 4, "timer = 0" + line 32, "pan.___", state 5, "avdelay = -(1)" + line 32, "pan.___", state 6, "lastpulse = 0" + line 36, "pan.___", state 12, "timer = 0" + line 37, "pan.___", state 13, "avdelay = -(1)" + line 37, "pan.___", state 14, "lastpacedpulsev = 0" + line 38, "pan.___", state 15, "lastpulse = 0" + line 47, "pan.___", state 28, "avdelay = 0" + line 48, "pan.___", state 29, "lastpacedpulsea = 0" + line 52, "pan.___", state 35, "avdelay = (avdelay+50)" + line 57, "pan.___", state 47, "-end-" + (11 of 47 states) +unreached in proctype environment + line 68, "pan.___", state 5, "lastpulse = timer" + line 68, "pan.___", state 6, "avdelay = 0" + line 68, "pan.___", state 8, "lastpulse = timer" + line 68, "pan.___", state 9, "avdelay = 0" + line 68, "pan.___", state 10, "pula = 1" + line 68, "pan.___", state 10, "timer = 0" + line 71, "pan.___", state 14, "avdelay = -(1)" + line 71, "pan.___", state 16, "avdelay = -(1)" + line 71, "pan.___", state 17, "pulv = 1" + line 71, "pan.___", state 17, "timer = 0" + line 82, "pan.___", state 30, "lastpulse = timer" + line 82, "pan.___", state 31, "avdelay = 0" + line 82, "pan.___", state 32, "pula = 1" + line 86, "pan.___", state 36, "avdelay = -(1)" + line 86, "pan.___", state 37, "timer = 0" + line 111, "pan.___", state 73, "-end-" + (14 of 73 states) +unreached in proctype sensor + line 117, "pan.___", state 3, "sena = 1" + line 117, "pan.___", state 4, "pula = 0" + line 123, "pan.___", state 23, "-end-" + (3 of 23 states) +unreached in proctype pacegen + line 133, "pan.___", state 5, "lastpacedpulsev = timer" + line 133, "pan.___", state 6, "avdelay = -(1)" + line 133, "pan.___", state 7, "pulv = 1" + line 143, "pan.___", state 20, "lastpacedpulsea = timer" + line 143, "pan.___", state 21, "avdelay = 0" + line 143, "pan.___", state 22, "pula = 1" + line 152, "pan.___", state 34, "pulv = 1" + line 152, "pan.___", state 35, "lastpacedpulsev = timer" + line 152, "pan.___", state 36, "avdelay = -(1)" + line 160, "pan.___", state 47, "lastpacedpulsev = timer" + line 160, "pan.___", state 48, "avdelay = -(1)" + line 165, "pan.___", state 55, "lastpacedpulsev = timer" + line 165, "pan.___", state 56, "avdelay = -(1)" + line 165, "pan.___", state 57, "pulv = 1" + line 173, "pan.___", state 69, "lastpacedpulsea = timer" + line 173, "pan.___", state 70, "avdelay = 0" + line 178, "pan.___", state 77, "lastpacedpulsea = timer" + line 178, "pan.___", state 78, "avdelay = 0" + line 178, "pan.___", state 79, "pula = 1" + line 199, "pan.___", state 114, "pulsea!1" + line 199, "pan.___", state 115, "lastpacedpulsea = timer" + line 199, "pan.___", state 116, "avdelay = 0" + line 199, "pan.___", state 117, "sensea?_" + line 203, "pan.___", state 121, "lastpacedpulsea = timer" + line 203, "pan.___", state 122, "avdelay = 0" + line 212, "pan.___", state 136, "avdelay = 0" + line 212, "pan.___", state 137, "sensea?_" + line 216, "pan.___", state 141, "lastpacedpulsev = timer" + line 216, "pan.___", state 142, "avdelay = -(1)" + line 216, "pan.___", state 143, "sensev?_" + line 218, "pan.___", state 146, "lastpacedpulsev = timer" + line 218, "pan.___", state 147, "avdelay = -(1)" + line 218, "pan.___", state 148, "pulsev!1" + line 226, "pan.___", state 165, "-end-" + (34 of 165 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 298, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.03 seconds +pan: rate 105000 states/second +pan: avg transition delay 6.4364e-06 usec +0.00user 0.01system 0:00.07elapsed 32%CPU (0avgtext+0avgdata 12880maxresident)k +0inputs+16outputs (0major+845minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/XDD.ltl b/verified_pacemaker/XDD.ltl new file mode 100644 index 0000000..8254ac9 --- /dev/null +++ b/verified_pacemaker/XDD.ltl @@ -0,0 +1,124 @@ +#define p sena == 1 +#define q avdelay <= avd +#define r senv == 0 +#define s pulv == 1 + + /* + * Formula As Typed: [] (p -><> (q && r && s)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -><> (q && r && s))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -><> (q && r && s))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (! ((s)) && (p)))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (! ((s))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 295) +depth 1455: Claim reached state 9 (line 300) +depth 1587: Claim reached state 9 (line 300) + +(Spin Version 5.2.5 -- 17 April 2010) + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 96 byte, depth reached 3679, errors: 0 + 2440 states, stored (3354 visited) + 1168 states, matched + 4522 transitions (= visited+matched) + 3 atomic steps +hash conflicts: 6 (resolved) + +Stats on memory usage (in Megabytes): + 0.261 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.458 actual memory usage for states (unsuccessful compression: 175.63%) + state-vector as stored = 181 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 0.305 memory used for DFS stack (-m10000) + 2.696 total actual memory usage + +unreached in proctype updatetimers + line 31, "pan.___", state 4, "timer = 0" + line 32, "pan.___", state 5, "avdelay = -(1)" + line 32, "pan.___", state 6, "lastpulse = 0" + line 57, "pan.___", state 47, "-end-" + (4 of 47 states) +unreached in proctype environment + line 85, "pan.___", state 34, "lastpulse = timer" + line 85, "pan.___", state 35, "avdelay = 0" + line 85, "pan.___", state 36, "pula = 1" + line 89, "pan.___", state 40, "avdelay = -(1)" + line 89, "pan.___", state 41, "timer = 0" + line 101, "pan.___", state 54, "lastpulse = timer" + line 101, "pan.___", state 55, "avdelay = 0" + line 101, "pan.___", state 56, "timer = 0" + line 105, "pan.___", state 60, "avdelay = -(1)" + line 105, "pan.___", state 61, "timer = 0" + line 113, "pan.___", state 78, "-end-" + (11 of 78 states) +unreached in proctype sensor + line 131, "pan.___", state 37, "-end-" + (1 of 37 states) +unreached in proctype pacegen + line 159, "pan.___", state 34, "lastpacedpulsev = timer" + line 159, "pan.___", state 35, "avdelay = -(1)" + line 164, "pan.___", state 42, "lastpacedpulsev = timer" + line 164, "pan.___", state 43, "avdelay = -(1)" + line 164, "pan.___", state 44, "pulv = 1" + line 172, "pan.___", state 56, "lastpacedpulsea = timer" + line 172, "pan.___", state 57, "avdelay = 0" + line 177, "pan.___", state 64, "lastpacedpulsea = timer" + line 177, "pan.___", state 65, "avdelay = 0" + line 177, "pan.___", state 66, "pula = 1" + line 185, "pan.___", state 78, "pulv = 1" + line 185, "pan.___", state 79, "lastpacedpulsev = timer" + line 185, "pan.___", state 80, "avdelay = -(1)" + line 190, "pan.___", state 87, "lastpacedpulsev = timer" + line 190, "pan.___", state 88, "avdelay = -(1)" + line 190, "pan.___", state 89, "pulv = 1" + line 198, "pan.___", state 101, "pula = 1" + line 198, "pan.___", state 102, "lastpacedpulsea = timer" + line 198, "pan.___", state 103, "avdelay = 0" + line 203, "pan.___", state 110, "lastpacedpulsea = timer" + line 203, "pan.___", state 111, "avdelay = 0" + line 203, "pan.___", state 112, "pula = 1" + line 221, "pan.___", state 141, "pulv = 1" + line 221, "pan.___", state 142, "lastpacedpulsev = timer" + line 221, "pan.___", state 143, "avdelay = -(1)" + line 228, "pan.___", state 159, "-end-" + (26 of 159 states) +unreached in proctype :init: + (0 of 6 states) +unreached in proctype :never: + line 302, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.03 seconds +pan: rate 111800 states/second +pan: avg transition delay 6.6342e-06 usec +0.00user 0.02system 0:00.06elapsed 40%CPU (0avgtext+0avgdata 12912maxresident)k +0inputs+8outputs (0major+848minor)pagefaults 0swaps + +#endif diff --git a/verified_pacemaker/XDD_H.ltl b/verified_pacemaker/XDD_H.ltl new file mode 100644 index 0000000..5339ce2 --- /dev/null +++ b/verified_pacemaker/XDD_H.ltl @@ -0,0 +1,156 @@ +#define p sena == 1 +#define q avdelay <= avd +#define r senv == 0 +#define s pulv == 1 +#define t responsefactor == 10 + + /* + * Formula As Typed: [] (p -><> (q && r && s && t)) + * The Never Claim Below Corresponds + * To The Negated Formula !([] (p -><> (q && r && s && t))) + * (formalizing violations of the original) + */ + +never { /* !([] (p -><> (q && r && s && t))) */ +T0_init: + if + :: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (((! ((s)) && (p)) || (! ((t)) && (p)))))))) -> goto accept_S3 + :: (1) -> goto T0_init + fi; +accept_S3: + if + :: (((! ((q))) || (((! ((r))) || (((! ((s))) || (! ((t))))))))) -> goto accept_S3 + fi; +} + +#ifdef NOTES +Use Load to open a file or a template. + + + + +#endif +#ifdef RESULT +warning: for p.o. reduction to be valid the never claim must be stutter-invariant +(never claims generated from LTL formulae are stutter-invariant) +depth 0: Claim reached state 5 (line 384) +depth 1742: Claim reached state 9 (line 389) +depth 1924: Claim reached state 9 (line 389) +pan:1: acceptance cycle (at depth 1742) +pan: wrote pan_in.trail + +(Spin Version 5.2.5 -- 17 April 2010) +Warning: Search not completed + + Partial Order Reduction + +Full statespace search for: + never claim + + assertion violations + (if within scope of claim) + acceptance cycles + (fairness disabled) + invalid end states - (disabled by never claim) + +State-vector 116 byte, depth reached 4587, errors: 1 + 2746 states, stored (3200 visited) + 442 states, matched + 3642 transitions (= visited+matched) + 4 atomic steps +hash conflicts: 0 (resolved) + +Stats on memory usage (in Megabytes): + 0.346 equivalent memory usage for states (stored*(State-vector + overhead)) + 0.446 actual memory usage for states (unsuccessful compression: 129.00%) + state-vector as stored = 154 byte + 16 byte overhead + 2.000 memory used for hash table (-w19) + 3.052 memory used for DFS stack (-m100000) + 5.442 total actual memory usage + +unreached in proctype updatetimers + line 40, "pan.___", state 4, "timer = 0" + line 41, "pan.___", state 5, "avdelay = -(1)" + line 41, "pan.___", state 6, "lastpulse = 0" + line 66, "pan.___", state 47, "-end-" + (4 of 47 states) +unreached in proctype environment + line 83, "pan.___", state 18, "avdelay = -(1)" + line 83, "pan.___", state 20, "avdelay = -(1)" + line 83, "pan.___", state 21, "pulv = 1" + line 83, "pan.___", state 21, "timer = 0" + line 94, "pan.___", state 34, "lastpulse = timer" + line 94, "pan.___", state 35, "avdelay = 0" + line 94, "pan.___", state 36, "pula = 1" + line 98, "pan.___", state 40, "avdelay = -(1)" + line 98, "pan.___", state 41, "timer = 0" + line 110, "pan.___", state 54, "lastpulse = timer" + line 110, "pan.___", state 55, "avdelay = 0" + line 110, "pan.___", state 56, "timer = 0" + line 114, "pan.___", state 60, "avdelay = -(1)" + line 114, "pan.___", state 61, "timer = 0" + line 122, "pan.___", state 78, "-end-" + (14 of 78 states) +unreached in proctype sensor + line 140, "pan.___", state 41, "-end-" + (1 of 41 states) +unreached in proctype pacegen + line 154, "pan.___", state 14, "pulv = 1" + line 154, "pan.___", state 15, "lastpacedpulsev = timer" + line 154, "pan.___", state 16, "avdelay = -(1)" + line 168, "pan.___", state 39, "pula = 1" + line 168, "pan.___", state 40, "lastpacedpulsea = timer" + line 168, "pan.___", state 41, "avdelay = 0" + line 176, "pan.___", state 54, "lastpacedpulsev = timer" + line 176, "pan.___", state 55, "avdelay = -(1)" + line 177, "pan.___", state 57, "responsefactor = 10" + line 186, "pan.___", state 69, "pulv = 1" + line 186, "pan.___", state 70, "lastpacedpulsev = timer" + line 186, "pan.___", state 71, "avdelay = -(1)" + line 188, "pan.___", state 77, "pulv = 1" + line 188, "pan.___", state 78, "lastpacedpulsev = timer" + line 188, "pan.___", state 79, "avdelay = -(1)" + line 184, "pan.___", state 80, "(((mode==VVIR)||(mode==DDIR)))" + line 184, "pan.___", state 80, "else" + line 196, "pan.___", state 92, "lastpacedpulsea = timer" + line 196, "pan.___", state 93, "avdelay = 0" + line 197, "pan.___", state 95, "responsefactor = 10" + line 206, "pan.___", state 107, "pula = 1" + line 206, "pan.___", state 108, "lastpacedpulsea = timer" + line 206, "pan.___", state 109, "avdelay = 0" + line 208, "pan.___", state 115, "pula = 1" + line 208, "pan.___", state 116, "lastpacedpulsea = timer" + line 208, "pan.___", state 117, "avdelay = 0" + line 204, "pan.___", state 118, "(((mode==AAIR)||(mode==DDIR)))" + line 204, "pan.___", state 118, "else" + line 216, "pan.___", state 130, "pulv = 1" + line 216, "pan.___", state 131, "lastpacedpulsev = timer" + line 216, "pan.___", state 132, "avdelay = -(1)" + line 221, "pan.___", state 139, "lastpacedpulsev = timer" + line 221, "pan.___", state 140, "avdelay = -(1)" + line 221, "pan.___", state 141, "pulv = 1" + line 229, "pan.___", state 153, "pula = 1" + line 229, "pan.___", state 154, "lastpacedpulsea = timer" + line 229, "pan.___", state 155, "avdelay = 0" + line 234, "pan.___", state 162, "lastpacedpulsea = timer" + line 234, "pan.___", state 163, "avdelay = 0" + line 234, "pan.___", state 164, "pula = 1" + line 255, "pan.___", state 199, "pulv = 1" + line 255, "pan.___", state 200, "lastpacedpulsev = timer" + line 255, "pan.___", state 201, "avdelay = -(1)" + line 262, "pan.___", state 217, "-end-" + (42 of 217 states) +unreached in proctype accelerometer + line 280, "pan.___", state 24, "responsefactor = 6" + line 280, "pan.___", state 26, "responsefactor = 5" + line 287, "pan.___", state 41, "responsefactor = 8" + line 287, "pan.___", state 43, "responsefactor = 9" + line 294, "pan.___", state 59, "-end-" + (5 of 59 states) +unreached in proctype :init: + (0 of 8 states) +unreached in proctype :never: + line 391, "pan.___", state 11, "-end-" + (1 of 11 states) + +pan: elapsed time 0.498 seconds +pan: rate 6425.7028 states/second +pan: avg transition delay 0.00013674 usec + +#endif diff --git a/verified_pacemaker/pacemaker.c b/verified_pacemaker/pacemaker.c new file mode 100644 index 0000000..8016720 --- /dev/null +++ b/verified_pacemaker/pacemaker.c @@ -0,0 +1,400 @@ +#include +#include +#include +#include + +/* Globals */ +int timer=0; +int sena = 0; +int senv = 0; +int pula = 0; +int pulv = 0; +int avd = 150; +int avdelay = -1; +int lastpulse = 0; +int lastpacedpulsea = 0; +int lastsenseda = 0; +int lastpacedpulsev =0; +int lastsensedv = 0; +int maxtime = 1000; +int mintime = 500; +int nr = 830; +int sensortime = 500; +int incrementtime = 50; +int responsefactor = 5; +int hysteresistime = 1000; +int hysteresis = 0; +int vrp =320; +int arp =250; +int pvarp = 250; +int schd = 1; +enum behave {nondet,dead,missv}; +enum m {VOO, AOO, VVI, AAI, VVT, AAT, DOO, DDI,DDD,VDD,AOOR,AAIR,VOOR,VVIR,VDDR,DOOR,DDIR,DDDR,all}; +enum activity {low,med,high}; + +/* Generated by Control Refinement */ + +void updatetimers() +{ +if (timer>=0) +timer = timer+50; +if (avdelay == -1 && lastpulse >0) +{ +timer = 0; +avdelay=-1; +lastpulse=0; +} +if(lastpacedpulsev >0 && lastpulse >0) +{ +timer =0; +avdelay=-1; +lastpacedpulsev=0; +lastpulse=0; +} +if(lastpacedpulsev >0) +{ +avdelay=-1; +lastpacedpulsev=0; +} +if(lastpacedpulsea >0) +{ +avdelay=0; +lastpacedpulsea=0; +} +if(avdelay>=0) +avdelay = avdelay+50; +} + +void environment(enum behave b) +{ +if(b == nondet) +{ +/* Normal Non Deterministic Heart */ +if((timer - lastpulse) >= nr) +{ +pula=1; +lastpulse = timer;avdelay=0; +} + +if( avdelay >= avd) +{ +pulv=1; +avdelay=-1; +} + +} +if(b == missv) +{ +/* Missing Ventricle Pulse Heart */ +if((timer - lastpulse) >= nr) +{ +pula = 1; +lastpulse = timer; +avdelay=0; +} + +if(avdelay >= avd) +{ +/*::pulsev!1;avdelay=-1;*/ +timer =0; +avdelay=-1; +} +} + +if(b == dead) +{ +/* Dead Heart */ + +if((timer - lastpulse) >= nr) +{ +/*::pulsea!1;lastpulse = timer;avdelay=0;*/ +timer=0; +lastpulse = timer; +avdelay=0; +} + +if(avdelay >= avd) +{ +/*::pulsev!1;avdelay=-1;*/ +timer =0; +avdelay=-1; +} +} +} + +void sensor() +{ + +if(pula ==1 && sena ==1) +{ +sena=0; +pula=0; +} + +if(pula ==1) +{ +sena = 1; +pula =0; +lastsenseda = timer; +} +else +{ +sena = 0; +lastsenseda = 0; +} + +if(pulv ==1 && senv ==1) +{ +senv=0; +pulv=0; +} + +if(pulv==1) +{ +senv =1; +pulv=0; +lastsensedv = timer; +} +else +{ +senv =0; +lastsensedv = 0; +} + +} + +void pacegen(enum m mode) +{ + +if(mode == VOO || mode == DOO || mode == DDD|| mode == VDD || mode == VOOR || mode == DOOR || mode == DDDR || mode == VDDR) +{ + +if((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime ) + +if(mode == VOOR || mode == DOOR || mode == DDDR || mode == VDDR) +{ + +if((timer - lastpacedpulsev) >= (sensortime + responsefactor*incrementtime)) +{ +pulv =1; +lastpacedpulsev = timer; +avdelay=-1; +} +} +else +{ +pulv = 1; +lastpacedpulsev = timer; +avdelay=-1; +} +} + +if(mode == AOO || mode == DOO || mode == DDD || mode == AOOR || mode == DOOR || mode == DDDR) +{ + +if((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime ) + +if(mode ==AOOR ||mode == DOOR || mode == DDDR) +{ + +if((timer - lastpacedpulsea) >= (sensortime + responsefactor*incrementtime)) +{ +pula =1; +lastpacedpulsea = timer; +avdelay=0; +} +} +else +{ +pula =1; +lastpacedpulsea = timer; +avdelay=0; +} +} + +if(mode == VVI || mode == DDI || mode == VVIR || mode == DDIR ) +{ + +if(senv == 1 && timer - lastpacedpulsev > vrp) +{ +lastpacedpulsev = timer; +avdelay = -1; +} + +if(hysteresis == 1) +responsefactor = 10; + +if((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime ) + +if(mode == VVIR || mode == DDIR ) +{ + +if((timer - lastpacedpulsev) >= (sensortime + responsefactor*incrementtime)) +{ +pulv =1; +lastpacedpulsev = timer; +avdelay=-1; +} +} +else +{ +pulv = 1; +lastpacedpulsev = timer; +avdelay=-1; +} +} + +if(mode == AAI || mode == DDI || mode == AAIR ||mode == DDIR) +{ + +if(sena ==1 && timer - lastpacedpulsea > arp) +{ +lastpacedpulsea = timer; +avdelay=0; +} + +if(hysteresis == 1) +responsefactor = 10; + +if((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime ) + +if(mode == AAIR ||mode == DDIR) +{ + +if ((timer - lastpacedpulsea) >= (sensortime + responsefactor*incrementtime)) +{ +pula =1; +lastpacedpulsea = timer; +avdelay=0; +} +} +else +{ +pula=1; +lastpacedpulsea = timer; +avdelay=0; +} +} + +if(mode == VVT && timer - lastpacedpulsev > vrp) +{ + +if(senv==1) +{ +pulv=1; +lastpacedpulsev = timer; +avdelay=-1; +} + +if((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime ) +{ +pulv=1; +lastpacedpulsev = timer; +avdelay=-1; +} +} + +if(mode == AAT && timer - lastpacedpulsea > arp) +{ + +if (sena == 1) +{ +pula = 1; +lastpacedpulsea = timer; +avdelay=0; +} + +if((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime ) +{ +pula=1; +lastpacedpulsea = timer; +avdelay=0; +} +} + +if(mode == DDD || mode == VDD ||mode ==VDDR ||mode == DDDR) +{ + +if(sena == 1 && timer - lastpacedpulsev > pvarp) +avdelay=0; + +if(hysteresis == 1) +responsefactor = 10; + +if(senv == 1 && timer - lastpacedpulsev > pvarp) +avdelay=-1; +} + +if(mode == DOO || mode == DDI || mode ==VDD || mode == DDD ||mode ==DOOR || mode == DDIR || mode == VDDR ||mode ==DDDR) +{ + +if(avdelay >= avd) +{ +pulv =1; +lastpacedpulsev = timer; +avdelay=-1; +} +} + +} + +void accelerometer(enum activity act) +{ + +if(act == low) +{ + +if(responsefactor > 3) +responsefactor = 3; + +if(responsefactor == 3) +responsefactor = 2; + +if(responsefactor == 2) +responsefactor = 1; +} + +if(act == med) +{ + +if(responsefactor > 6) +responsefactor = 6; + +if(responsefactor == 6) +responsefactor = 5; + +if(responsefactor <= 5) +responsefactor = 4; +} + +if(act == high) +{ + +if(responsefactor < 7) +responsefactor = 7; + +if(responsefactor == 7) +responsefactor = 8; + +if(responsefactor == 8) +responsefactor = 9; +} + +} + +void main() +{ +enum behave b = nondet; +enum m mode = DDD; +enum activity act = low; +int hysteresis = 1; + +while(1) +{ +updatetimers(); +environment(b); +sensor(); +accelerometer(act); +pacegen(mode); +} +} diff --git a/verified_pacemaker/pacemaker.h b/verified_pacemaker/pacemaker.h new file mode 100644 index 0000000..aff431c --- /dev/null +++ b/verified_pacemaker/pacemaker.h @@ -0,0 +1,31 @@ +/* Header File with Globals */ +/* Generated from Data Refinement */ + +int timer = 0; +int sena = 0; +int senv = 0; +int pula = 0; +int pulv = 0; +int avd = 150; +int avdelay = -1; +int lastpulse = 0; +int lastpacedpulsea = 0; +int lastsenseda = 0; +int lastpacedpulsev =0; +int lastsensedv = 0; +int maxtime = 1000; +int mintime = 500; +int nr = 830; +int sensortime = 500; +int incrementtime = 50; +int responsefactor = 5; +int hysteresistime = 1000; +int hysteresis = 0; +int vrp =320; +int arp =250; +int pvarp = 250; +int schd = 1; +enum behave {nondet,dead,missv}; +enum m {VOO, AOO, VVI, AAI, VVT, AAT, DOO, DDI,DDD,VDD,AOOR,AAIR,VOOR,VVIR,VDDR,DOOR,DDIR,DDDR,all}; +enum activity {low,med,high}; +/*End Data Refinement*/ \ No newline at end of file diff --git a/verified_pacemaker/pacemaker_C_Code.pml b/verified_pacemaker/pacemaker_C_Code.pml new file mode 100644 index 0000000..40a9824 --- /dev/null +++ b/verified_pacemaker/pacemaker_C_Code.pml @@ -0,0 +1,321 @@ +int timer=0; +chan pulsea = [0] of {bit}; +chan pulsev = [0] of {bit}; +chan sensea = [0] of {bit}; +chan sensev = [0] of {bit}; +bit sena = 0; +bit senv = 0; +bit pula = 0; +bit pulv = 0; +int avd = 150; +int avdelay = -1; +int lastpulse = 0; +int lastpacedpulsea = 0; +int lastsenseda = 0; +int lastpacedpulsev =0; +int lastsensedv = 0; +int maxtime = 1000; +int mintime = 500; +int nr = 830; +int sensortime = 500; +int incrementtime = 50; +int responsefactor = 5; +int hysteresistime = 1000; +int hysteresis = 0; +int vrp =320; +int arp =250; +int pvarp = 250; +int schd = 1; +mtype = { nondet,dead,missv }; +mtype = { VOO, AOO, VVI, AAI, VVT, AAT, DOO, DDI,DDD,VDD,AOOR,AAIR,VOOR,VVIR,VDDR,DOOR,DDIR,DDDR }; +mtype = {low,med,high}; +c_code{#include "pacemaker.h"}; +int imode = 0; +int endstate = 0; + +proctype updatetimers() +{ +do +::(timer>=0 && schd ==1)-> timer = timer+50; +if +::(avdelay == -1 && lastpulse >0)-> +timer = 0; +avdelay=-1; +lastpulse=0; +::else->skip; +fi; +if +::(lastpacedpulsev >0 && lastpulse >0)-> +timer =0; +avdelay=-1; +lastpacedpulsev=0; +lastpulse=0; +::else->skip; +fi; +if +::(lastpacedpulsev >0)-> +avdelay=-1; +lastpacedpulsev=0; +::else->skip; +fi; +if +::(lastpacedpulsea >0)-> +avdelay=0; +lastpacedpulsea=0; +::else->skip; +fi; +if +::(avdelay>=0)-> +avdelay = avdelay+50; +::else -> skip; +fi; +if +::(schd == 1) -> schd = 2; +fi; +od; +} +proctype environment(mtype b) +{ +do +::(schd == 2) -> +if +::(b == nondet) -> +/* Normal Non Deterministic Heart */ +if +::((timer - lastpulse) >= nr)-> +if +::pula=1;lastpulse = timer;avdelay=0; +::timer = 0;lastpulse = timer;avdelay=0; +fi; +::else ->skip; +fi; +if +::(avdelay >= avd)-> +if +::pulv=1;avdelay=-1; +::timer =0;avdelay=-1; +fi; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(b == missv) -> +/* Missing Ventricle Pulse Heart */ +if +::((timer - lastpulse) >= nr)-> +if +::pula = 1;lastpulse = timer;avdelay=0; +fi; +::(avdelay >= avd)-> +if +/*::pulsev!1;avdelay=-1;*/ +::timer =0;avdelay=-1; +fi; +::else -> skip; +fi; +::else ->skip +fi; +if +::(b == dead) -> +/* Dead Heart */ +if +::((timer - lastpulse) >= nr)-> +if +/*::pulsea!1;lastpulse = timer;avdelay=0;*/ +::timer=0;lastpulse = timer;avdelay=0; +fi; +::(avdelay >= avd)-> +if +/*::pulsev!1;avdelay=-1;*/ +::timer =0;avdelay=-1; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(schd == 2) -> schd = 3; +fi +od; +} +proctype sensor() +{ +do +::(schd == 3)-> +if +::(pula ==1 && sena ==1) -> sena=0; pula=0; +::else ->skip; +fi; +if +::(pula ==1) -> sena = 1;pula =0;lastsenseda = timer; +::else -> sena = 0;lastsenseda = 0; +fi; +if +::(pulv ==1 && senv ==1) -> senv=0; pulv=0; +::else -> skip; +fi; +if +::(pulv==1) -> senv =1;pulv=0;lastsensedv = timer; +::else -> senv =0;lastsensedv = 0; +fi; +if +::(schd == 3) -> schd = 4; +fi; +od; +} +proctype pacegen(mtype mode) +{ +do +::(schd == 5) -> +c_code +{ +enum m mode = now.imode; +int hysteresis = now.hysteresis; +if(mode == VOO || mode == DOO || mode == DDD|| mode == VDD || mode == VOOR || mode == DOOR || mode == DDDR || mode == VDDR) +{ +if((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime ) +if(mode == VOOR || mode == DOOR || mode == DDDR || mode == VDDR) +{ +if((timer - lastpacedpulsev) >= (sensortime + responsefactor*incrementtime)) +{pulv =1;lastpacedpulsev = timer;avdelay=-1;} +} +else { pulv = 1;lastpacedpulsev = timer;avdelay=-1; } +} + +if(mode == AOO || mode == DOO || mode == DDD || mode == AOOR || mode == DOOR || mode == DDDR) +{ +if((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime ) +if(mode ==AOOR ||mode == DOOR || mode == DDDR) +{ +if((timer - lastpacedpulsea) >= (sensortime + responsefactor*incrementtime)) +{pula =1;lastpacedpulsea = timer;avdelay=0;} +} +else {pula =1;lastpacedpulsea = timer;avdelay=0;} +} + +if(mode == VVI || mode == DDI || mode == VVIR || mode == DDIR ) +{ +if(senv == 1 && timer - lastpacedpulsev > vrp) {lastpacedpulsev = timer; avdelay = -1;} +if(hysteresis == 1) responsefactor = 10; +if((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime ) +if(mode == VVIR || mode == DDIR ) +{ +if((timer - lastpacedpulsev) >= (sensortime + responsefactor*incrementtime)) {pulv =1;lastpacedpulsev = timer;avdelay=-1;} +} +else {pulv = 1;lastpacedpulsev = timer;avdelay=-1;} +} + +if(mode == AAI || mode == DDI || mode == AAIR ||mode == DDIR) +{ +if(sena ==1 && timer - lastpacedpulsea > arp) {lastpacedpulsea = timer;avdelay=0;} +if(hysteresis == 1) responsefactor = 10; +if((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime ) +if(mode == AAIR ||mode == DDIR) +{ +if ((timer - lastpacedpulsea) >= (sensortime + responsefactor*incrementtime)) {pula =1;lastpacedpulsea = timer;avdelay=0;} +} +else {pula=1;lastpacedpulsea = timer;avdelay=0;} +} + +if(mode == VVT && timer - lastpacedpulsev > vrp) +{ +if(senv==1) { pulv=1;lastpacedpulsev = timer;avdelay=-1;} +if((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime ) +{ +pulv=1;lastpacedpulsev = timer;avdelay=-1; +} +} +if(mode == AAT && timer - lastpacedpulsea > arp) +{ +if (sena == 1) {pula = 1;lastpacedpulsea = timer;avdelay=0;} +if((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime ) +{ +pula=1;lastpacedpulsea = timer;avdelay=0; +} +} + +if(mode == DDD || mode == VDD ||mode ==VDDR ||mode == DDDR) +{ +if(sena == 1 && timer - lastpacedpulsev > pvarp) avdelay=0; +if(hysteresis == 1) responsefactor = 10; +if(senv == 1 && timer - lastpacedpulsev > pvarp) avdelay=-1; +} +if(mode == DOO || mode == DDI || mode ==VDD || mode == DDD ||mode ==DOOR || mode == DDIR || mode == VDDR ||mode ==DDDR) +{ +if(avdelay >= avd) {pulv =1;lastpacedpulsev = timer;avdelay=-1;} +} +now.hysteresis = hysteresis; +now.lastpacedpulsea =lastpacedpulsea; +now.lastpacedpulsev = lastpacedpulsev; +now.avdelay = avdelay; +now.pulv=pulv; +now.pula=pula; +now.senv=senv; +now.sena = sena; +now.responsefactor = responsefactor; +}; +endstate =1; +if +::(schd == 5) -> schd = 1; +fi; +od; +} +proctype accelerometer() +{ +do +::(schd == 4) -> +mtype act ; +if +::act = low; +::act=med; +::act=high; +fi; +if +::(act == low)-> +if +::(responsefactor > 3) -> responsefactor = 3; +::(responsefactor == 3) -> responsefactor = 2; +::(responsefactor == 2)-> responsefactor = 1; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(act == med)-> +if +::(responsefactor > 6) -> responsefactor = 6; +::(responsefactor == 6) -> responsefactor = 5; +::(responsefactor <= 5) -> responsefactor = 4; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(act == high)-> +if +::(responsefactor < 7) -> responsefactor = 7; +::(responsefactor == 7) -> responsefactor = 8; +::(responsefactor == 8)-> responsefactor = 9; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(schd == 4) -> schd = 5; +fi; +od; +} +init +{ +mtype behave = nondet; +mtype mode = nondet; +hysteresis = 1; +atomic{ +run updatetimers(); +run environment(behave); +run sensor(); +run accelerometer(); +run pacegen(mode); +} +} diff --git a/verified_pacemaker/pacemaker_concurrent.pml b/verified_pacemaker/pacemaker_concurrent.pml new file mode 100644 index 0000000..c18f668 --- /dev/null +++ b/verified_pacemaker/pacemaker_concurrent.pml @@ -0,0 +1,224 @@ +int timer=0; +int maxtimer = 1000; +chan pulsea = [0] of {bit}; +chan pulsev = [0] of {bit}; +bit sensea=0; +bit sensev=0; +int avd = 150; +int avdelay = -1; +int lastpulsea = 0; +int lastpulsev = 0; +int lastpacedpulsev = 0; +int lastpacedpulsea = 0; +int maxtime = 1000; +int mintime = 500; +int nr = 830; +mtype = {VOO,AOO,VVI,AAI,DDI,DOO,AAT,VVT,VDD,DDD}; +mtype = {normal,missv,dead,nondet}; + +proctype sensor() +{ +do +::pulsea?_->sensea=1; +::pulsev?_->sensev=1; +od; +} + +proctype environment(mtype behave) +{ +do +::(behave == nondet) -> +if +::behave = normal; +::behave = missv; +::behave = dead; +fi; + +::(behave == normal)-> + +if +::(timer - lastpulsea >= nr && avdelay == -1)-> +pulsea!1;lastpulsea =timer; avdelay=0; +::else ->skip; +fi; + +if +::(avdelay >= avd)-> +pulsev!1;lastpulsev=timer;avdelay=-1; +::else -> skip; +fi; + +if +::(timer >=0 && timer < maxtimer)-> +timer =timer +50; +::else ->skip; +fi; + +if +::(avdelay >=0 && avdelay/10 == 0)-> +avdelay = avdelay +50; +::else ->skip; +fi; + +if +::(timer >= maxtimer && (lastpacedpulsev >0 && lastpacedpulsea>0))-> +avdelay = -1; +lastpulsea = 0; +lastpulsev = 0; +lastpacedpulsev = 0; +lastpacedpulsea = 0; +timer = 0; +::else ->skip; +fi; + +::(behave == missv)-> + +if +::((timer - lastpulsea >= nr && avdelay == -1) )-> +pulsea!1;lastpulsea =timer; avdelay=0; +::else ->skip; +fi; + +if +::(avdelay >= avd)-> +avdelay=-1; +::else -> skip; +fi; + +if +::(timer >=0 && timer < maxtimer)-> +timer =timer +50; +::else ->skip; +fi; + +if +::(avdelay >=0 && avdelay/10 == 0)-> +avdelay = avdelay +50; +::else ->skip; +fi; + +if +::(timer >= maxtimer && (lastpacedpulsev >0 && lastpacedpulsea>0))-> +avdelay = -1; +lastpulsea = 0; +lastpulsev = 0; +lastpacedpulsev = 0; +lastpacedpulsea = 0; +timer = 0; +::else ->skip; +fi; + +::(behave == dead)-> + +if +::((timer - lastpulsea >= nr && avdelay == -1))-> +avdelay = 0; +::else ->skip; +fi; + +if +::(avdelay >= avd)-> +avdelay=-1; +::else -> skip; +fi; + +if +::(timer >=0 && timer < maxtimer)-> +timer =timer +50; +::else ->skip; +fi; + +if +::(avdelay >= 0 && avdelay/10 == 0)-> +avdelay = avdelay +50; +::else -> skip; +fi; + +if +::(timer >= maxtimer && (lastpacedpulsev >0 && lastpacedpulsea>0))-> +avdelay = -1; +lastpulsea = 0; +lastpulsev = 0; +lastpacedpulsev = 0; +lastpacedpulsea = 0; +timer = 0; +::else ->skip; +fi; +od; +} + +proctype pacegen(mtype mode) +{ +do +::(mode == nondet) -> +if +::mode = AOO; +::mode = VOO; +::mode = AAI; +::mode = VVI; +::mode = AAT; +::mode = VVT; +::mode = DOO; +::mode = DDI; +::mode = DDD; +::mode = VDD; +fi; +::(mode == VOO || mode == DOO|| mode == VVI || mode == DDI || mode == VVT || mode == VDD || mode == DDD)-> +if +::((timer -lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime) -> +pulsev!1;lastpacedpulsev=timer;avdelay =-1; +::else ->skip; +fi; +::(mode == AOO || mode == DOO || mode ==AAI ||mode == DDI || mode == AAT || mode == DDD)-> +if +::((timer -lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime) -> +pulsea!1;lastpacedpulsea=timer;avdelay =0; +::else ->skip; +fi; +::(mode == VDD|| mode == DDD)-> +if +::(avdelay >=avd) -> +pulsev!1;lastpacedpulsev=timer;avdelay =-1; +::else ->skip; +fi; +::(mode == VVI || mode == DDI)-> +if +::(sensev == 1)-> sensev=0;avdelay =-1; +::else -> skip; +fi; +::( mode == AAI || mode == DDI)-> +if +::(sensea == 1)-> sensea=0;avdelay =0; +::else -> skip; +fi; +::(mode == VVT)-> +if +::(sensev == 1) -> pulsev!1;lastpacedpulsev=timer;avdelay =-1;sensev=0; +::else ->skip; +fi; +::(mode == AAT)-> +if +::(sensea == 1) -> pulsea!1;lastpacedpulsea=timer;avdelay =0;sensea=0; +::else ->skip; +fi; +::(mode == VDD || mode == DDD)-> +if +::(sensea==1) -> sensea=0; avdelay =0; +::else ->skip; +fi; +if +::(sensev == 1)-> sensev=0;avdelay =-1; +::else -> skip; +fi; +od; +} +init +{ +mtype mode = nondet; +mtype behave =nondet; +atomic{ +run environment(behave); +run sensor(); +run pacegen(mode); +} +} diff --git a/verified_pacemaker/pacemaker_distributed.pml b/verified_pacemaker/pacemaker_distributed.pml new file mode 100644 index 0000000..af0dc13 --- /dev/null +++ b/verified_pacemaker/pacemaker_distributed.pml @@ -0,0 +1,243 @@ +int timer=0; +int pacedtimer =0; +int maxtimer = 1000; +chan pulsea = [0] of {bit}; +chan pulsev = [0] of {bit}; +chan sensea = [0] of {bit}; +chan sensev = [0] of {bit}; +chan syncavd = [0] of {int}; +int avd = 150; +int avdelay = -1; +int pacedavdelay = -1; +int lastpulsea = 0; +int lastpulsev = 0; +int lastpacedpulsev = 0; +int lastpacedpulsea = 0; +int maxtime = 1000; +int mintime = 500; +int nr = 830; +mtype = {VOO,AOO,VVI,AAI,DDI,DOO,AAT,VVT,VDD,DDD}; +mtype = {normal,missv,dead,nondet}; +int synctime =0; + +proctype sensor() +{ +do +::pulsea?_->sensea!1; +::pulsev?_->sensev!1; +od; +} + +proctype environment(mtype behave) +{ +do + +::(behave == nondet) -> +if +::behave = normal; +::behave = missv; +::behave = dead; +fi; + +::(behave == normal)-> + +if +::(timer - lastpulsea >= nr && avdelay == -1)-> +pulsea!1;lastpulsea =timer; avdelay=0; +::else ->skip; +fi; + +if +::(avdelay >= avd)-> +pulsev!1;lastpulsev=timer;avdelay=-1; +::else -> skip; +fi; + +if +::(timer >=0 && timer < maxtimer)-> +timer =timer +50; +::else ->skip; +fi; + +if +::(avdelay >=0 && avdelay/10 == 0)-> +avdelay = avdelay +50; +syncavd ! avdelay; +::else ->skip; +fi; + +if +::(timer >= maxtimer && (lastpacedpulsev >0 && lastpacedpulsea>0))-> +avdelay = -1; +lastpulsea = 0; +lastpulsev = 0; +timer = 0; +::else ->skip; +fi; + +::(behave == missv)-> + +if +::(timer - lastpulsea >= nr && avdelay == -1)-> +pulsea!1;lastpulsea =timer; avdelay=0; +::else ->skip; +fi; + +if +::(avdelay >= avd)-> +avdelay=-1; +::else -> skip; +fi; + +if +::(timer >=0 && timer < maxtimer)-> +timer =timer +50; +::else ->skip; +fi; + +if +::(avdelay >=0 && avdelay/10 == 0)-> +avdelay = avdelay +50; +syncavd ! avdelay; +::else ->skip; +fi; + +if +::(timer >= maxtimer && (lastpacedpulsev >0 && lastpacedpulsea>0))-> +avdelay = -1; +lastpulsea = 0; +lastpulsev = 0; +timer = 0; +::else ->skip; +fi; +::(behave == dead)-> + +if +::(timer - lastpulsea >= nr && avdelay == -1)-> + avdelay=0; +::else ->skip; +fi; + +if +::(avdelay >= avd)-> +avdelay=-1; +::else -> skip; +fi; + +if +::(timer >=0 && timer < maxtimer)-> +timer =timer +50; +::else ->skip; +fi; + +if +::(avdelay >=0 && avdelay/10 == 0)-> +avdelay = avdelay +50; +syncavd ! avdelay; +::else ->skip; +fi; + +if +::(timer >= maxtimer && (lastpacedpulsev >0 && lastpacedpulsea>0))-> +avdelay = -1; +lastpulsea = 0; +lastpulsev = 0; +timer = 0; +::else ->skip; +fi; + +od; +} + +proctype pacegen(mtype mode) +{ +do +::(mode == nondet) -> +if +::mode = AOO; +::mode = VOO; +::mode = AAI; +::mode = VVI; +::mode = AAT; +::mode = VVT; +::mode = DOO; +::mode = DDI; +::mode = DDD; +::mode = VDD; +fi; + +::(mode == VOO || mode == DOO|| mode == VVI || mode == DDI || mode == VVT || mode == VDD || mode == DDD)-> +if +::((pacedtimer -lastpacedpulsev) > mintime && (pacedtimer - lastpacedpulsev) < maxtime) -> +lastpacedpulsev=pacedtimer; +::else ->skip; +fi; +::(mode == AOO || mode == DOO|| mode == AAI || mode == DDI || mode == AAT || mode == DDD)-> +if +::((pacedtimer - lastpacedpulsea) > mintime && (pacedtimer - lastpacedpulsea) < maxtime) -> +lastpacedpulsea=pacedtimer; +::else ->skip; +fi; +::(mode == VVI || mode == DDI)-> +if +::sensev?_-> pacedtimer = 0; +::skip; +fi; +::(mode == AAI || mode == DDI)-> +if +::sensea?_-> pacedtimer = 0; +::skip; +fi; +::(mode == VVT)-> +if +::sensev?_-> lastpacedpulsev = timer; +::skip; +fi; +::(mode == AAT)-> +if +::sensea?_-> lastpacedpulsea = timer; +::skip; +fi; +::(mode == VDD || mode == DDD)-> +if +::sensea?_->pacedavdelay = 0; +::sensev?_->pacedtimer = 0;pacedavdelay =-1; +::skip; +fi; +::(mode == VDD || mode == DDD)-> +if +::(pacedavdelay >= avd)-> +lastpacedpulsev=pacedtimer;pacedavdelay=-1; +::else -> skip; +fi; +::(mode == VOO || mode == DOO|| mode == VVI || mode == DDI || mode == VVT || mode == VDD || mode == DDD || mode == AOO || mode == DOO|| mode == AAI || mode == DDI || mode == AAT || mode == DDD)-> +if +::(pacedtimer >=0 && pacedtimer < maxtimer)-> +pacedtimer =pacedtimer +50; +::else ->skip; +fi; +if +::(pacedavdelay >=0)-> +::syncavd ? synctime -> pacedavdelay = synctime; +::skip; +fi; +if +::(pacedtimer >= maxtimer && (lastpacedpulsev >0 && lastpacedpulsea>0))-> +lastpacedpulsev = 0; +lastpacedpulsea = 0; +pacedtimer = 0; +pacedavdelay=-1; +::else ->skip; +fi; +od; +} +init +{ +mtype mode =nondet; +mtype behave = nondet; +atomic{ +run environment(behave); +run sensor(); +run pacegen(mode); +} +} diff --git a/verified_pacemaker/pacemaker_sequential.pml b/verified_pacemaker/pacemaker_sequential.pml new file mode 100644 index 0000000..59ffc3f --- /dev/null +++ b/verified_pacemaker/pacemaker_sequential.pml @@ -0,0 +1,389 @@ +int timer=0; +chan pulsea = [0] of {bit}; +chan pulsev = [0] of {bit}; +chan sensea = [0] of {bit}; +chan sensev = [0] of {bit}; +bit sena = 0; +bit senv = 0; +bit pula = 0; +bit pulv = 0; +int avd = 150; +int avdelay = -1; +int lastpulse = 0; +int lastpacedpulsea = 0; +int lastsenseda = 0; +int lastpacedpulsev =0; +int lastsensedv = 0; +int maxtime = 1000; +int mintime = 500; +int nr = 830; +int sensortime = 500; +int incrementtime = 50; +int responsefactor = 5; +int hysteresistime = 1000; +int hysteresis = 0; +int vrp =320; +int arp =250; +int pvarp = 250; +int schd = 1; +mtype = { nondet,dead,missv }; +mtype = { VOO, AOO, VVI, AAI, VVT, AAT, DOO, DDI,DDD,VDD,AOOR,AAIR,VOOR,VVIR,VDDR,DOOR,DDIR,DDDR }; +mtype = {low,med,high}; + + +proctype updatetimers() +{ +do +::(timer>=0 && schd ==1)-> timer = timer+50; +if +::(avdelay == -1 && lastpulse >0)-> +timer = 0; +avdelay=-1; +lastpulse=0; +::else->skip; +fi; +if +::(lastpacedpulsev >0 && lastpulse >0)-> +timer =0; +avdelay=-1; +lastpacedpulsev=0; +lastpulse=0; +::else->skip; +fi; +if +::(lastpacedpulsev >0)-> +avdelay=-1; +lastpacedpulsev=0; +::else->skip; +fi; +if +::(lastpacedpulsea >0)-> +avdelay=0; +lastpacedpulsea=0; +::else->skip; +fi; +if +::(avdelay>=0)-> +avdelay = avdelay+50; +::else -> skip; +fi; +if +::(schd == 1) -> schd = 2; +fi; +od; +} +proctype environment(mtype b) +{ +do +::(schd == 2) -> +if +::(b == nondet) -> +/* Normal Non Deterministic Heart */ +if +::((timer - lastpulse) >= nr)-> +if +::pula=1;lastpulse = timer;avdelay=0; +::timer = 0;lastpulse = timer;avdelay=0; +fi; +::else ->skip; +fi; +if +::(avdelay >= avd)-> +if +::pulv=1;avdelay=-1; +::timer =0;avdelay=-1; +fi; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(b == missv) -> +/* Missing Ventricle Pulse Heart */ +if +::((timer - lastpulse) >= nr)-> +if +::pula = 1;lastpulse = timer;avdelay=0; +fi; +::(avdelay >= avd)-> +if +/*::pulsev!1;avdelay=-1;*/ +::timer =0;avdelay=-1; +fi; +::else -> skip; +fi; +::else ->skip +fi; +if +::(b == dead) -> +/* Dead Heart */ +if +::((timer - lastpulse) >= nr)-> +if +/*::pulsea!1;lastpulse = timer;avdelay=0;*/ +::timer=0;lastpulse = timer;avdelay=0; +fi; +::(avdelay >= avd)-> +if +/*::pulsev!1;avdelay=-1;*/ +::timer =0;avdelay=-1; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(schd == 2) -> schd = 3; +fi +od; +} +proctype sensor() +{ +do +::(schd == 3)-> +if +::(pula ==1 && sena ==1) -> sena=0; pula=0; +::else ->skip; +fi; +if +::(pula ==1) -> sena = 1;pula =0;lastsenseda = timer; +::else -> sena = 0;lastsenseda = 0; +fi; +if +::(pulv ==1 && senv ==1) -> senv=0; pulv=0; +::else -> skip; +fi; +if +::(pulv==1) -> senv =1;pulv=0;lastsensedv = timer; +::else -> senv =0;lastsensedv = 0; +fi; +if +::(schd == 3) -> schd = 4; +fi; +od; +} +proctype pacegen(mtype mode) +{ +do +::(schd == 5) -> +if +::(mode == nondet) -> +if +::mode = AOO; +::mode = VOO; +::mode = AAI; +::mode = VVI; +::mode = AAT; +::mode = VVT; +::mode = DOO; +::mode = DDI; +::mode = DDD; +::mode = VDD; +::mode = AOOR; +::mode = VOOR; +::mode = AAIR; +::mode = VVIR; +::mode = DOOR; +::mode = VDDR; +::mode = DDIR; +::mode = DDDR; +fi; +::else -> skip ; +fi; +if +::(mode == VOO || mode == DOO || mode == DDD|| mode == VDD || mode == VOOR || mode == DOOR || mode == DDDR || mode == VDDR)-> +if +::((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime )-> +if +::(mode == VOOR || mode == DOOR || mode == DDDR || mode == VDDR) -> +if +::((timer - lastpacedpulsev) >= (sensortime + responsefactor*incrementtime))->pulv =1;lastpacedpulsev = timer;avdelay=-1; +::else->skip; +fi; +::else -> pulv =1;lastpacedpulsev = timer;avdelay=-1; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(mode == AOO || mode == DOO || mode == DDD || mode == AOOR || mode == DOOR || mode == DDDR)-> +if +::((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime )-> +if +::(mode ==AOOR ||mode == DOOR || mode == DDDR) -> +if +::((timer - lastpacedpulsea) >= (sensortime + responsefactor*incrementtime))->pula =1;lastpacedpulsea = timer;avdelay=0; +::else->skip; +fi; +::else -> pula =1;lastpacedpulsea = timer;avdelay=0; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(mode == VVI || mode == DDI || mode == VVIR || mode == DDIR )-> +if +::(senv == 1 && timer - lastpacedpulsev > vrp) -> lastpacedpulsev = timer; avdelay = -1; +if +::(hysteresis == 1) -> responsefactor = 10; +::else->skip; +fi; +::else -> skip; +fi; +if +::((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime )-> +if +::(mode == VVIR || mode == DDIR )-> +if +::((timer - lastpacedpulsev) >= (sensortime + responsefactor*incrementtime))->pulv =1;lastpacedpulsev = timer;avdelay=-1; +::else ->skip; +fi; +::else -> pulv = 1;lastpacedpulsev = timer;avdelay=-1; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(mode == AAI || mode == DDI || mode == AAIR ||mode == DDIR)-> +if +::(sena ==1 && timer - lastpacedpulsea > arp) ->lastpacedpulsea = timer;avdelay=0; +if +::(hysteresis == 1) -> responsefactor = 10; +::else->skip; +fi; +::else -> skip; +fi; +if +::((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime )-> +if +::(mode == AAIR ||mode == DDIR)-> +if +::((timer - lastpacedpulsea) >= (sensortime + responsefactor*incrementtime))->pula =1;lastpacedpulsea = timer;avdelay=0; +::else -> skip; +fi; +::else ->pula=1;lastpacedpulsea = timer;avdelay=0; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(mode == VVT) -> +if +::(senv==1 && timer-lastpacedpulsev > vrp) -> pulv=1;lastpacedpulsev = timer;avdelay=-1; +::else -> skip; +fi; +if +::((timer - lastpacedpulsev) > mintime && (timer - lastpacedpulsev) < maxtime )-> +if +::pulv=1;lastpacedpulsev = timer;avdelay=-1; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(mode == AAT) -> +if +::(sena == 1 && timer-lastpacedpulsea > arp) -> pula = 1;lastpacedpulsea = timer;avdelay=0; +::else -> skip; +fi; +if +::((timer - lastpacedpulsea) > mintime && (timer - lastpacedpulsea) < maxtime )-> +if +::pula=1;lastpacedpulsea = timer;avdelay=0; +fi; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(mode == DDD || mode == VDD ||mode ==VDDR ||mode == DDDR) -> +if +::(sena == 1 && timer-lastpacedpulsev > pvarp) ->avdelay=0; +if +::(hysteresis == 1) -> responsefactor = 10; +::else->skip; +fi; +::else -> skip; +fi; +if +::(senv == 1 && timer-lastpacedpulsev > pvarp) -> avdelay=-1; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(mode == DOO || mode == DDI || mode ==VDD || mode == DDD ||mode ==DOOR || mode == DDIR || mode == VDDR ||mode ==DDDR) -> +if +::(avdelay >= avd)-> pulv =1;lastpacedpulsev = timer;avdelay=-1; +::else -> skip; +fi; +::else -> skip; +fi; +if +::(schd == 5) -> schd = 1; +fi; +od; +} +proctype accelerometer() +{ +do +::(schd == 4) -> +mtype act ; +if +::act = low; +::act=med; +::act=high; +fi; +if +::(act == low)-> +if +::(responsefactor > 3) -> responsefactor = 3; +::(responsefactor == 3) -> responsefactor = 2; +::(responsefactor == 2)-> responsefactor = 1; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(act == med)-> +if +::(responsefactor > 6) -> responsefactor = 6; +::(responsefactor == 6) -> responsefactor = 5; +::(responsefactor <= 5) -> responsefactor = 4; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(act == high)-> +if +::(responsefactor < 7) -> responsefactor = 7; +::(responsefactor == 7) -> responsefactor = 8; +::(responsefactor == 8)-> responsefactor = 9; +::else -> skip; +fi; +::else ->skip; +fi; +if +::(schd == 4) -> schd = 5; +fi; +od; +} +init +{ +mtype behave = nondet; +mtype mode = nondet; +hysteresis = 1; +atomic{ +run updatetimers(); +run environment(behave); +run sensor(); +run accelerometer(); +run pacegen(mode); +} +}