readme.md

RTS

AADL Architecture

System: RTS_i_Instance

Thread: actuator
Classifier: Actuation::Actuator.i
Periodic: 1000 ms
Domain: 14

Thread: actuator
Classifier: Actuation::Actuator.i
Periodic: 1000 ms
Domain: 16

Thread: coincidenceLogic
Classifier: Actuation::CoincidenceLogic.i
Periodic: 1000 ms
Domain: 5

Thread: coincidenceLogic
Classifier: Actuation::CoincidenceLogic.i
Periodic: 1000 ms
Domain: 6

Thread: coincidenceLogic
Classifier: Actuation::CoincidenceLogic.i
Periodic: 1000 ms
Domain: 7

Thread: coincidenceLogic
Classifier: Actuation::CoincidenceLogic.i
Periodic: 1000 ms
Domain: 9

Thread: coincidenceLogic
Classifier: Actuation::CoincidenceLogic.i
Periodic: 1000 ms
Domain: 10

Thread: coincidenceLogic
Classifier: Actuation::CoincidenceLogic.i
Periodic: 1000 ms
Domain: 11

Thread: orLogic
Classifier: Actuation::OrLogic.i
Periodic: 1000 ms
Domain: 8

Thread: orLogic
Classifier: Actuation::OrLogic.i
Periodic: 1000 ms
Domain: 12

Thread: orLogic
Classifier: Actuation::OrLogic.i
Periodic: 1000 ms
Domain: 13

Thread: orLogic
Classifier: Actuation::OrLogic.i
Periodic: 1000 ms
Domain: 15

Thread: actuatorsMockThread
Classifier: Actuators::ActuatorsMockThread.i
Periodic: 1000 ms
Domain: 4

Thread: eventControlMockThread
Classifier: EventControl::EventControlMockThread.i
Periodic: 1000 ms
Domain: 3

Thread: instrumentationMockThread
Classifier: Instrumentation::InstrumentationMockThread.i
Periodic: 1000 ms
Domain: 2

Logika

The following reports the experimental data obtained by running Logika only on the component entrypoints that require verification (e.g. TempControl's Fan component was excluded as it does not contain GUMBO contracts and does not use datatypes that have invariants). Logika was configured with a 2 second validity checking timeout, a 500 millisecond satisfiability checking timeout, a SMT2 resource limit of 2,000,000, and with full parallelization optimizations enabled. The SMT2 solvers used include CVC4 1.8, CVC5 1.0.5, and Z3 4.12.2. The VC and SAT columns report the number of verification and satisfiability conditions that were checked, respectively. The time values reported in the final three columns are the averages obtained after re-running Logika 25 times for each entrypoint on an M1 Mac Mini with 8 cores and 16 GB of RAM. TTime gives the total number of seconds it took to run Logika from the command line on the Slang project containing the entrypoint (i.e. it includes the verification time along with the time required for parsing, type checking, etc.).

One optimization technique related to using Logika from within IVE that can be measured via our experimental setup is Sireum's incremental type checking. For example, if Logika was run on the Isolette MA component's initialize entrypoint from within IVE using an identical configuration as was done for the experiments then it will take on average 2.482 seconds to verify, assuming Logika had not previously been invoked. If a change was then made to MA's source code before re-running Logika on the timeTriggered entrypoint then Sireum's incremental type checking will only need to recheck MA (and any of its dependents) resulting in an average delay of only 0.214 seconds before verification can proceed. The results of these optimizations are reported in the Incremental-Type Checking column (ITCTime). The time required to actually verify an entrypoint with a clean cache is reported in the Verification-Time column (VTime) so incremental type checking for this example would save 2.268 seconds (2.482 - 0.214) on average.

Results

coincidenceLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.258	0.174	3
timeTriggered	5	0	2.462	0.168	0.230

coincidenceLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.235	0.173	3
timeTriggered	5	0	2.433	0.170	0.228

coincidenceLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.246	0.172	3
timeTriggered	5	0	2.471	0.168	0.231

orLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.242	0.169	3
timeTriggered	3	0	2.340	0.173	0.112

coincidenceLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.248	0.174	3
timeTriggered	5	0	2.454	0.171	0.228

coincidenceLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.240	0.169	3
timeTriggered	5	0	2.443	0.169	0.230

coincidenceLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.250	0.172	3
timeTriggered	5	0	2.464	0.171	0.230

orLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.235	0.168	3
timeTriggered	3	0	2.343	0.168	0.113

orLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.227	0.172	3
timeTriggered	3	0	2.330	0.171	0.112

actuator

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	1	0	2.260	0.170	0.029
timeTriggered	3	0	2.330	0.172	0.114

orLogic

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	0	0	2.234	0.165	3
timeTriggered	3	0	2.336	0.168	0.112

actuator

Raw Data: csv

EntryPoint	VC	SAT	TTime	ITCTime	VTime
initialise	1	0	2.293	0.175	0.029
timeTriggered	3	0	2.354	0.173	0.115

How to replicate

To run the experiments, first install Sireum Kekinian (optionally choosing the commit tip used for the experiments, ie. 843ede1)

git clone --rec https://github.com/sireum/kekinian.git
cd kekinian
git checkout 843ede1
git pull --rec
bin/build.cmd

export SIREUM_HOME=$(pwd)
export PATH=$SIREUM_HOME/bin:$PATH

Then run the following Slash script specifying the number of number of times to rerun Logika on each entrypoint: ../bin/report-logika.cmd

../bin/report-logika.cmd run 25

The results will be appended to the csv file corresponding to the component being evaluated. The line val projects: Map[String, Project] = Map.empty + isolette + rts + tcP + tcS in the script can be modified if you want to run a subset of the projects