This article presents AutoFocus, a tool prototype for formally based development of distributed, embedded systems. AutoFocus supports system development offering integrated, comprehensive and mainly graphical description techniques to specify different views as well as different levels of abstraction of a system. To avoid ill-defined specifications, consistency conditions on these system descriptions can be formulated and checked. Prototypes can be generated from consistent and executable specifications. These prototypes can be executed and visualized within a simulation environment. For formal verification of specification properties, common model checkers can be used with AutoFocus.     «

This article presents AutoFocus, a tool prototype for formally based development of distributed, embedded systems. AutoFocus supports system development offering integrated, comprehensive and mainly graphical description techniques to specify different views as well as different levels of abstraction of a system. To avoid ill-defined specifications, consistency conditions on these system descriptions can be formulated and checked. Prototypes can be generated from consistent and executable specif...     »