Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 SEFROS
Symbolic Execution Based Formal Reasoning About Open Systems
This project is funded by the Swedish Research Council (VR) and
effectively started in August 2003.
Project Description
Formal methods. Nowadays computers have entered almost all
spheres of society. Being linked in a vast network, they provide not only
a facility for information storage and manipulation, but also a medium
for communication and information exchange. The globalization of information
has been accompanied by a growth in the number of applications requiring
secure operation and availability, such as in electronic commerce, telecommunications
and safety critical systems. This development has lead to such high a level
of complexity of understanding, designing and exploiting such applications,
which can only be dealt with by using sophisticated analysis and design
techniques with solid mathematical and logical foundations, known collectively
as
formal methods. These methods are supported by powerful semantics
based tools, such as the SPIN tool of AT&T, for the description
and analysis of both hardware and software through facilities for simulation,
debugging, testing, and even verification - the activity of formally
proving systems correct. Formal analysis techniques are based on formal
models of the behaviour of the analysed systems.
Open systems. A particular class of systems are the so-called
open
systems, where software components can dynamically enter a system,
interact with other components, and then exit the system. Open systems
are built on top of open programming platforms which provide the necessary
functionalities. Due to their flexibility, open platforms are becoming
indispensable in many areas. One example are smart cards, where
the ambition of smart card providers is to allow new applications to be
loaded on a smart card after the card has been issued, and to allow these
newly loaded applications to interact with other applications on the smart
card. A standard example are loyalty partnership applications in electronic
purses. An example for a multi-application smart card open platform is
JavaCard by Sun.
The challenges. Open systems are particularly challenging
to be reasoned about, since one has to analyse the behaviour of the system
without knowing all its components, but rather by relying on certain behavioural
properties of the unknown components. It is maybe of little surprise that
the existing widespread formal methods tools do not support well reasoning
about open systems. For this to become possible, one has first to develop
the semantic foundations of open systems by providing adequate notions
for their operation (symbolic execution) in terms of symbolic states and
transitions, relatevised on the assumptions about the behaviour of the
unknown components.
The goals. The goals of the project are:
to introduce and explore a suitable notion of relativised symbolic state
capturing the assumptions on the component parameters, together with suitable
equivalence
notions;
to develop the necessary mathematical machinery for efficient symbolic
execution (that is, symbolic next-state generation) and reasoning about
behaviours of open systems;
to evaluate the theoretical investigations by implementing a demonstrator
tool in the tradition of SPIN, but for the simulation and verification
of open systems, enhanced with novel debugging facilities like temporal
debugging, and by conducting relevant case studies, possibly
taken from the multi-application smart card application area.