Formal Verification of Embedded Systems Using the Alvis Approach
Embedded systems are usually characterized by time-critical reactions and increased complexity. Because it is usually impossible to correct a system bug by simply uploading of a new version of a system software or firmware, a system behavior should be verified in a formal manner. The Alvis approach presented in this paper is able to verify the system behavior, by specifying the border between a developed embedded system and its environment. The means to move the border is then proposed, which allows the designer to create a formal representation for selected parts of a model only.
Daizhong Su, Kai Xue and Shifan Zhu
L. Kotulski and M. Szpyrka, "Formal Verification of Embedded Systems Using the Alvis Approach", Key Engineering Materials, Vol. 486, pp. 209-212, 2011