TY - GEN
T1 - Automated validation of IoT device control programs through domain-specific model generation
AU - Choi, Yunja
N1 - Publisher Copyright:
© Springer International Publishing AG, part of Springer Nature 2018.
PY - 2018
Y1 - 2018
N2 - The IoT is a networked system of physical devices controlled by embedded software whose validity is a pre-requisite to ensuring the correct behavior of the entire system. To automate the verification and validation process of such control software, this work constructs a validation model by composing pre-defined behavioral patterns of an operating system that is compliant with the OSEK/VDX international standard and models of application programs abstracted w.r.t. interactions with the underlying operating system. This validation model is used to perform property checking using the model checker SPIN to ensure that the behavior of the control program complies with the original intention of the program design. We automated the model generation process and applied it to 9 benchmark programs for the open source IoT OS Erika.
AB - The IoT is a networked system of physical devices controlled by embedded software whose validity is a pre-requisite to ensuring the correct behavior of the entire system. To automate the verification and validation process of such control software, this work constructs a validation model by composing pre-defined behavioral patterns of an operating system that is compliant with the OSEK/VDX international standard and models of application programs abstracted w.r.t. interactions with the underlying operating system. This validation model is used to perform property checking using the model checker SPIN to ensure that the behavior of the control program complies with the original intention of the program design. We automated the model generation process and applied it to 9 benchmark programs for the open source IoT OS Erika.
UR - http://www.scopus.com/inward/record.url?scp=85049035246&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-92970-5_16
DO - 10.1007/978-3-319-92970-5_16
M3 - Conference contribution
AN - SCOPUS:85049035246
SN - 9783319929699
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 254
EP - 268
BT - Software Engineering and Formal Methods - 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Proceedings
A2 - Johnsen, Einar Broch
A2 - Schaefer, Ina
PB - Springer Verlag
T2 - 16th International Conference on Software Engineering and Formal Methods, SEFM 2018 Held as Part of STAF 2018
Y2 - 27 June 2018 through 29 June 2018
ER -