TY - GEN
T1 - Local model update with an application to sliding window protocol
AU - Kelly, Michael
AU - Zhang, Yan
PY - 2010
Y1 - 2010
N2 - Local model update is a procedure whereby a property is found unsatisfied in some model and can be effectively made satisfied in the error reporting counterexample through a series of modifications. With this the counterexample can be reintegrated into the original model to derive a global fix. In this paper we put forward the case for local model update as a method for automatic update. We review theory underlying local model update and introduce the use of a tool lmu for automatically generating candidate updates, looking at general design principles. Finally we present a case study of the update process as applied to an abstraction of the sliding window protocol under a man-in-the-middle attack, showing the modelling process, update procedure and final derivation of a coherant model fix.
AB - Local model update is a procedure whereby a property is found unsatisfied in some model and can be effectively made satisfied in the error reporting counterexample through a series of modifications. With this the counterexample can be reintegrated into the original model to derive a global fix. In this paper we put forward the case for local model update as a method for automatic update. We review theory underlying local model update and introduce the use of a tool lmu for automatically generating candidate updates, looking at general design principles. Finally we present a case study of the update process as applied to an abstraction of the sliding window protocol under a man-in-the-middle attack, showing the modelling process, update procedure and final derivation of a coherant model fix.
UR - http://handle.uws.edu.au:8081/1959.7/562475
UR - http://kes2010.kesinternational.org/
U2 - 10.1007/978-3-642-15384-6_2
DO - 10.1007/978-3-642-15384-6_2
M3 - Conference Paper
SN - 9783642153839
SP - 11
EP - 21
BT - Proceedings Knowledge-Based and Intelligent Information and Engineering Systems: 14th International Conference, KES 2010, Cardiff, UK, September 8-10, 2010
PB - Springer
T2 - International Conference on Knowledge-Based Intelligent Information and Engineering Systems
Y2 - 8 September 2010
ER -