[Pl-seminar] 6/1 Seminar: Cesare Tinelli, CoCoSpec: A Mode-aware Contract Language for Reactive Systems

[Daniel Patterson]

NUPRL Seminar presents

Cesare Tinelli
University of Iowa
Host: Thomas Wahl

11AM-12:30PM (NOTE: THIS IS EARLIER THAN OUR NORMAL TIME!)
Thursday, June 1st, 2017 (NOTE: THIS IS NOT OUR STANDARD DAY OF WEEK!)
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


CoCoSpec: A Mode-aware Contract Language for Reactive Systems

Abstract:

Contract-based software development is a leading methodology for the
construction of safety- and mission-critical embedded systems. Contracts
are an effective way to establish boundaries between components and can
be used efficiently to verify global properties by using compositional
reasoning techniques. A contract specifies the assumptions a component
makes on its context and the guarantees it provides. Requirements in the
specification of a component are often case-based, with each case
describing what the component should do depending on a specific
situation (or mode) the component is in.

This talk introduces CoCoSpec, a mode-aware assume-guarantee-based
contract language for embedded systems. CoCoSpec is built as an
extension of the Lustre language and lets users specify mode behavior
directly, instead of encoding it as conditional guarantees, thus
preventing a loss of mode-specific information. Mode-aware model
checkers supporting CoCoSpec can increase the effectiveness of the
compositional analysis techniques found in assume-guarantee frameworks
and improve scalability. Such tools can also produce much better
feedback during the verification process, as well as valuable
qualitative information on the contract itself. I will presents the
CoCoSpec language and illustrate the benefits of mode-aware
model-checking on a case study involving a flight-critical avionics
system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based
model checker developed at the University of Iowa that provides full
support for CoCoSpec.

Bio:

Cesare Tinelli received a Ph.D. in Computer Science from the UIUC in
1999 and is currently a professor in Computer Science at the University
of Iowa. His research interests include automated reasoning and formal
methods. He has done seminal work in automated reasoning, in particular
in Satisfiability Modulo Theories (SMT), a field he helped establish
through his research and service activities. His work has been funded
both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and
corporations (Intel, General Electric, Rockwell Collins, and United
Technologies) and has appeared in more than 70 refereed publications. He
is a founder and coordinator of the SMT-LIB initiative, an international
effort aimed at standardizing benchmarks and I/O formats for SMT
solvers. He has led the development of the award winning Darwin theorem
prover and the Kind model checker. He co-leads the development of CVC4,a
widely used and award winning SMT solver, and StarExec, a cross
community web-based service for the comparative evaluation of logic
solvers.