Safe compositional network sketches: formal framework

NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch assists system integrators in two types of activities: modeling and design. As a modol, it enables the abstraction of an existing system while retaining sufficient information about it to carry out future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis. The compositional analysis is based on a strongly-typed Domain-Spe...

• Type: Conference
• Year: 2010
• Where: HYBRID
• Authors: Azer Bestavros, Assaf J. Kfoury, Andrei Lapets, Michael J. Ocean
• Keywords: Compositional Analysis, Desirable Safety Properties, HYBRID 2010, Hybrid Systems, Safety Properties