Dynamic Software Updating (DSU) consists in updating running programs on the fly without any downtime. This feature is interesting in critical applications that must run continuously. Because updates may lead to safety errors and security breaches, the question of their correctness is raised. Formal methods are a rigorous means to ensure the high level of safety requested by such applications. The detection of points to perform safe updates is a critical issue in DSU. Indeed, an hazardous update point leads the updated system to erroneous and unexpected behavior. We present in this paper a mechanism to detect safe update points in DSU for Java Card applications. The mechanism is then formally verified using model checking against correctness properties: deadlock free, activeness safety and DSU-liveness.
CITATION STYLE
Lounas, R., Jafri, N., Legay, A., Mezghiche, M., & Lanet, J. L. (2017). A formal verification of safe update point detection in dynamic software updating. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10158 LNCS, pp. 31–45). Springer Verlag. https://doi.org/10.1007/978-3-319-54876-0_3
Mendeley helps you to discover research relevant for your work.