Industrial integration of graphical and formal specifications

摘要: Abstract This paper discusses an approach to formal methods technology exploitation which introduces notations into critical systems development processes. The provision of “Ω functions” that map graphical specifications axiomatic specifications, can then be subjected proof, is explored as a means achieving this goal. Such functions must treat useful subset the language and compatible with industrialized tools. Experiences in developing for industrial application are discussed by example mapping function known Ω1. maps statecharts Real Time Logic.