his 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).