Verificare: A Platform for Composable Verification with Application Toward SDN-Enabled Applications: Rick Skowyra, PhD Proposal

Starts:
1:00 pm on Monday, November 11, 2013
Ends:
1:30 pm on Monday, November 11, 2013
Location:
MCS 148
Abstract: In this proposal, we present ongoing work on Verificare, a verification platform being built to enable formal verification of SDNs as components of a larger system. Verificare allows rapid, high-level modelling and composition of an SDN with a larger system model via reusable, composable, and encapsulated sub-models referred to as agents (active processes) and environments (contexts for inter-action). English-language system requirements, including those relating to SLAs, safety, and security, can selected from a variety of included libraries and automatically bound to these modular components. Translation mechanisms to and from off-the-shelf verification tools leverage and make accessible existing work in formal methods to provide an expressive platform for automatically verifying the behavior of system models.