Résumé:
We present a framework for compositional
specification and verification of multi-
application programs. The framework consists
of a compositional program model (an adaptation
of earlier work by Thomas Jensen et al),
a temporal property specification language
based on the mu-calculus, and a Gentzen-style
proof system for proving correctness of
property decompositions. We discuss the
utility of the approach on an Electronic
Purse case study provided by Gemplus.
This ongoing work is taking place within the European VerifiCard project.
Retour au sommaire / Back to schedule