Static Analysis of Programs Using Omega Algebra with Tests
Recently, Kozen has proposed a framework based on Kleene algebra with tests for verifying that a program satisfies a security policy specified by a security automaton. A security automaton is used for the specification of linear safety properties on finite and infinite runs. This kind of property is very interesting for most common programs. However, it is not possible to specify liveness properties with security automata. In this paper, we use omega algebra with tests and automata on infinite words to extend the field of properties that can be handled by security automata in Kozen’s framework.
KeywordsRegular Expression Security Policy Liveness Property Trace Model Kripke Frame
Unable to display preview. Download preview PDF.
- 1.Bolduc, C.: Oméga-algèbre — Théorie et application en vérification de programmes. Forthcoming M.Sc. thesis, Université Laval, Québec, Canada (2006)Google Scholar
- 4.Cohen, E.: Omega algebra and concurrency control. Presentation made at the 56th meeting of the IFIP Working Group 2.1, Ameland, The Netherlands (2001)Google Scholar
- 5.Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering, pp. 411–420. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
- 7.Kozen, D.: Kleene algebra with tests and the static analysis of programs. Technical report 1915-2003, Computer Science Department, Cornell University (2003)Google Scholar
- 10.Safra, S.: Complexity of Automata on Infinite Objects. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel (1989)Google Scholar