Title :
Executable computational logics: combining formal methods and programming language based system design
Author_Institution :
Dept. of Comput. Sci., Univ. of Illinois at Urbana-Champaign, Urbana, IL, USA
Abstract :
An executable computational logic can provide the desired bridge between formal system properties and formal methods to verify them on the one hand, and executable models of system designs based on programming languages on the other. However, not all such logics are equally well suited for the task. This paper gives some requirements that seem important for a computational logic to be suitable in practice, and discusses the experience with rewriting logic, its Maude language implementation, and its formal tool environment, concluding that they seem to meet well those requirements.
Keywords :
formal logic; formal specification; formal verification; programming languages; rewriting systems; systems analysis; Maude language; design requirement; executable computational logic; executable model; formal method; formal tool environment; hardware system; programming language; rewriting logic; software system; system design; system property; system verification; Bridges; Computer languages; Computer science; Convergence; Hardware; Logic design; Logic programming; Mathematical model; Mathematics; Military computing;
Conference_Titel :
Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings. First ACM and IEEE International Conference on
Conference_Location :
Mont Saint Michel, France
Print_ISBN :
0-7695-1923-7
DOI :
10.1109/MEMCOD.2003.1210081
