TY - GEN
T1 - Extended algebraic state-transition diagrams
AU - Tidjon, Lionel Nganyewou
AU - Frappier, Marc
AU - Leuschel, Michael
AU - Mammar, Amel
N1 - Publisher Copyright:
© 2018 IEEE.
PY - 2018/12/27
Y1 - 2018/12/27
N2 - Algebraic State-Transition Diagrams (ASTDs) are extensions of common automata and statecharts that can be combined with process algebra operators like sequence, choice, guard and quantified synchronization. They were previously introduced for the graphical representation, specification and proof of information systems. In an attempt to use ASTDs to specify cyber-attack detection, we have identified a number of missing features in ASTDs. This paper extends the ASTD notation with state variables (attributes), actions on transitions, and a new operator called flow which corresponds to AND states in statecharts and is a compromise between interleaving and synchronization in process algebras. We provide a formal structured operational semantics of these extensions and illustrate its implementation in an OCaml-based interpreter called iASTD and the model checker ProB. Extended ASTDs are illustrated in a case study in cyber attack detection.
AB - Algebraic State-Transition Diagrams (ASTDs) are extensions of common automata and statecharts that can be combined with process algebra operators like sequence, choice, guard and quantified synchronization. They were previously introduced for the graphical representation, specification and proof of information systems. In an attempt to use ASTDs to specify cyber-attack detection, we have identified a number of missing features in ASTDs. This paper extends the ASTD notation with state variables (attributes), actions on transitions, and a new operator called flow which corresponds to AND states in statecharts and is a compromise between interleaving and synchronization in process algebras. We provide a formal structured operational semantics of these extensions and illustrate its implementation in an OCaml-based interpreter called iASTD and the model checker ProB. Extended ASTDs are illustrated in a case study in cyber attack detection.
KW - Algebraic state transition diagrams
KW - Cyber attack detection
KW - Formal methods
KW - Information systems
U2 - 10.1109/ICECCS2018.2018.00023
DO - 10.1109/ICECCS2018.2018.00023
M3 - Conference contribution
AN - SCOPUS:85061400999
T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
SP - 146
EP - 155
BT - Proceedings - 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018
Y2 - 12 December 2018 through 14 December 2018
ER -