Beyond Model Checking: Formal Specification and Verification
                    of Practical Mission-Critical Systems
                      FME-2001 Tutorial March 13th 2001

                           Dr. Ramesh Bharadwaj
                 Center for High Assurance Computer Systems
                         Naval Research Laboratory
                         Washington, DC 20375  USA


Experience Level: Intermediate. Basic knowledge of software engineering
principles and the role of specification and verification in the software
development life-cycle is assumed.


Overview

This tutorial introduces an industrial-strength specification notation
and method for the formal specification and verification of systems,
more specifically software-intensive embedded computer systems as typified
by safety-critical applications in the avionics, biomedical, aerospace,
railway, telecommunications, and automotive industries.  Attendees will
gain a basic understanding of the method for constructing precise and
unambiguous specifications that are easy to understand and change, and
that satisfy a number of application independent and application specific
properties such as consistency, completeness, safety, and security.
They will also gain an understanding of the issues involved in scalability, 
verifiability, modularity, readability, maintainability, implementability,
etc., of formal specifications, and will be exposed to automated tools
such as model checkers and theorem provers for verification and validation.

Beginning with an introduction to the theory and method underlying
our approach, this tutorial will include a hands-on application of
the method and tools to an embedded system derived from a practical
domain (avionics).


Target Audience

This tutorial is targeted to formal methods researchers, tool builders,
as well as practitioners interested in cost-effective solutions to
industrial problems.  This includes formal methods experts who want
to be exposed to the emerging new technology of automatic verification
of infinite-state systems, as well as domain experts interested in
applying existing technology and tools to practical specification
and verification problems.



Lecturer's Biography

Dr. Ramesh Bharadwaj holds the BE, ME, and PhD degrees in Electrical
and Computer Engineering.  His industrial experience includes several
years of software and hardware development, and software project
management.  He has held research and development positions at several
industrial and research organizations, including Philips Research
Laboratories, the Tata Institute of Fundamental Research, Stanford
University, Communications Research Laboratory, and AT&T Bell
Laboratories.  He is currently a researcher in Software Engineering at
the Naval Research Laboratory.  His research interests include methods
and tools for formal requirements specification, analysis, and
verification, automatic theorem proving, abstraction, model checking,
and decision procedures.