Analytical development and verification of control-intensive systems

摘要: Designs are created through a high-level to low-level transformation in the form of formal top-down development procedure based upon successive refinement. Starting with (abstract) model, such as abstraction protocol standard, successively more detailed models refinement, fashion which guarantees that properties verified at one level hold all levels abstraction. The refinements end "model" forms ultimate implementation protocol. In embodiment this invention, analysis/development apparatus creates unique C language code representation specified system is guaranteed carry out tasks when executed stored program controlled machine. another embodiment, used create "net list" for manufacturing system.