Real-time, embedded and/or critical systems are
everywhere. Telephone switches, robot controllers, anti-lock braking
systems, many medical systems, and air-traffic controllers are
examples of systems with real-time and safety-critical features.
Errors in real-time systems, in particular for safety-critical
applications such as airplane collision avoidance systems, are
potentially disastrous.
Real-time systems are reactive: they
perform their functions and continuously respond to external events
within a specified amount of time.
It has been a challenging topic
for software engineering researchers and theorists to develop
computer-aided verification techniques and tools to ensure that
real-time and safety-critical systems satisfy both functional
correctness requirements and timeliness requirements.
Researchers
explore the area by first modeling systems with some kind of machines
(i.e., automata). The verification problem is then reduced to
checking whether a machine satisfies various properties extracted
from the requirements of the system. If the verification fails,
counterexample should be generated in order to help in finding the
cause of the problem. This approach may also be applied to the
validation of the implemented system, by using counterexample
generation to derive functional test cases.
Among the
techniques and tools supporting this kind of verification and
validation activies, model checking has shown great potential and is
gaining widespread acceptance, also in the industry. Current model
checking techniques are, however, quite limited when dealing with
complex timing requirements. In our project, we plan to extend
current techniques and develop new tools for dealing with complex
properties of timed models. New approaches like the pattern
techniques [D01] and the reversal-bounded counter techniques
[DIBKS00] are very promising in such investigations.
On the
other hand, the typical models of real-time systems studied in
verification are essentially finite-state. These are good models, for
instance, for a hardware controller that controls an anti-lock
braking system, since the state of the controller, when the timing
information between states is ignored, has only a finite (but,
possibly, huge) number of possible choices, implemented in a digital
circuit.
Many real-time systems, however, are actually
infinite-state rather than finite-state. For instance, in a real-time
program with a procedure call, a call stack is maintained. Since the
stack may be arbitrarily high, the program represents an
infinite-state system even when time is excluded. Another example is
a real-time security protocol in charge of exchanging timestamps. In
this case, an unbounded message queue is needed.
Up to now, there
have been very few research efforts in studying verification problems
for infinite-state real-time systems. However, these efforts are
essential in establishing verification methodologies for many
software systems.
Our proposed work is to investigate the
verification and validation problems for infinite-state real-time
systems with complex timing requirements that cannot be dealt with by
the traditional techniques.
From a broader perspective, while
model-checking is not yet a standard practice in (real-time) software
design, its benefits are beginning to gain acceptance within the
industry.
Various industrial-strength tools for popular notations
such as Statecharts and SDL already incorporate model-checkers, often
allowing push-button verifications of a large set of predefined
properties (such as deadlock, race conditions, existence of
unreachable states, etc.).
Their use is now gaining ground in
industrial environments, especially for safety-critical systems. The
proposed research differs from most of the current research on
real-time verification, since its focus is on infinite-state
real-time systems with complex timing constraints instead of
finite-state real-time systems with simple constraints.
Therefore,
the results obtained will be a valuable contribution and a complement
to the current research and practice in real-time system
verification.
We plan to continue pursuing new models and
techniques and identifying new verifiable real-time systems, in order
to build, in cooperation with University of California and Washington
State University, a prototype of a verification library for analyzing
infinite-state real-time systems with complex timing
requirements.
The verification library could be interfaced to
other (real-time) verification tools, such as temporal logic or model
checking tools, and thus extend their usability to a broader range of
real-time applications.
The library will be a valuable
contribution and a complement to the current research on verification
of real-time systems and it will help software engineers to produce
real-time software systems faster, better and cheaper.
Model
checking techniques and other automata-theoretic approaches are not
only useful for verification and validation, but are potentially very
promising in other areas, such as static analysis of programs, since
they may replace or complement more traditional data-flow techniques.
Static analysis is becoming particularly important in allowing
efficient executions of programs on the coming generation of
Instruction Level Parallelism processors. Here an automata-theoretic
approach may allow the transformation of static analysis problems,
such as alias analysis, into reachability and model checking
problems. The proposed project will develop, in cooperation with
Harvard University, the Cambridge Research Lab (USA) and
STMicroelectronics, techniques and tools for static analysis to be
included in a standard compilation environment.
Keywords
|
1. |
verification and validation |
|
2. |
safety-critical software |
|
3. |
real-time software |
|
4. |
model checking |
|
5. |
automata theory |
|
6. |
Instruction Level Parallelism |
People
Principal Investigator: Pierluigi San Pietro
Other People: L. Breveglieri, A. Cherubini, S. Crespi Reghizzi
Cooperations with: Z. Dang, O. Ibarra
The main objective of the project is to develop
theory, techniques and tools to be combined in a platform supporting
the analysis, testing, verification and validation of safety-critical
systems with complex timing requirements.
We plan to build, in
cooperation with University of California at Santa Barbara and
Washington State University, a verification library based upon
automata-theoretic tools such as the pattern technique of [D01].
Models for real-time systems that will be studied may contain
both dense unbounded clocks and unbounded discrete data structures.
They include timed automata augmented with stacks (e.g., for
real-time programs with function calls), queues (e.g., communicating
protocols with timestamps), counters (i.e., integer variables),
etc.
The resulting library will be capable of handling complex
timing requirements. After developing proper interfaces, this library
can be integrated into existing real-time verification tools, making
them applicable to a broader range of real-time specifications.
The
library can also be built into other verifications tools for
infinite-state systems and make them useful for analyzing real-time
infinite-state systems with complex timing requirements.
During
this investigation, we also plan to study various infinite-state
models, (such as queues and stacks) assessing their importance for
modeling and verification of critical systems, with or without timing
requirements. If the results of this more esplorative studies
increase our understanding of infinite-state models, then analysis
algorithms and techniques may be proposed and incorporated into the
verification library.
Another objective of this project is to
develop tools and techniques for the static analysis of programs,
such as the liveness of variables and the aliasing of pointers, which
are needed in transformations for optimising and parallelising the
machine code. Recent advances in the design of microprocessor
architectures have introduced parallelism at the level of instruction
execution (called ILP, Instruction Level Parallelism). A challenge
for modern compilers is to efficiently parallelize machine code, to
allow efficient executions on ILP processors. Automata-theoretic
tools and model checking will be used to attack the problems, in
order to develop, in cooperation with Harvard University and ST
Microelectronics, theory, techniques and tools for static analysis,
to be included in a standard compiler environment such as SUIFF.
A
goal of our research is also the integration of the resulting
analysis toolkit with other less precise analysis tools, such as one
developed in our group. A model checking tool could be used to check
only those parts of a program that are found in need of greater
optimization and thus require more precision in the analysis.
All analysis, verification and validation tools
envisaged in this project will be mainly based on model checking
technology. Model checking is a key technique invented in the early
80s [CE81,CES86,SC85] that makes it possible to verify automatically
a finite-state transition system against a temporal property, by
exhaustively exploring the finite state space of the
system.
Model-checking can be used to check a reactive software
system (modeled as a finite-state transition system) against a
requirement (modeled as a temporal property).
This is potentially
extremely useful for software verification and validation and has
been already widely exploited for hardware checking.
There
are two main classes of model checking techniques that use very
different logics and algorithms:
1) CTL (Computation Tree Logic
[CES86]) model-checking is based on describing the behavior of the
system as a an unbounded tree of possible choices;
2) LTL (Linear
Time Temporal Logic [P77]) model-checking is based on describing the
behavior of the system as an infinite sequence of states.
There
are a number of (finite-state) model-checkers available, such as
1)
CTL model-checker SMV by McMillan [M93], whose great success in
hardware verification is mainly explained by the exploitation of a
symbolic representation of sets of states called Binary Decision
Diagrams (BDD) [B86];
2) LTL model-checker SPIN by Holzmann [H97],
whose applications to model checking of distributed software stem
from its on-the-fly construction of the set of reachable states and
from the adoption of a very convenient modeling language,
Promela.
Recent development in the area includes the
exploration of symbolic representations for a finite set of states
other than BDDs [B86].
For instance, BMC (Bounded Model-checking)
has been proposed by unfolding a finite-state transition system up to
a bounded length into a Boolean formula [BCCZ99a]. Debugging some
classes of temporal properties can be then reduced to checking the
satisfiability of the Boolean formula. The satisfiability checking
can be performed by very efficient SAT-solvers such as Grasp [MS99].
BMC has been used as a symbolic debugger for large finite-state
systems [BCCZ99b]. Another alternative representation of Boolean
formulas is Boolean Expression Diagrams (BEDs) [AH97]. A symbolic
model-checker using BEDs as well as SAT-solvers has been reported
[WBCG00] along with encouraging experimental results.
In
practice, CTL and LTL model-checkers suffer from the state-explosion
problem, since the size of the state space grows exponentially in the
number of variables and concurrent components of the
system.
Techniques to attack the problem include:
1) symmetry
reduction [ND96] by exploiting symmetric components in the system so
that only one permutation of the components must be checked;
2)
abstract interpretations [CGL94] by abstracting the system under
consideration into a smaller one while preserving the property to be
verified;
3) compositional/assume-guarantee reasoning [GL94,AH99]
by verifying each loosely independent modules;
4) partial order
[GW94] by looking at transitions whose execution order is insensitive
to the requirement; etc.
Abstraction has long been considered
an effective way to reduce the size of a transition system with
respect to a temporal property [CGL94]. For instance, Holzmann and
Smith report a model-extractor by which an abstract verification
model can be automatically built from C-code [H99]. Ball et al.
recently investigate how to construct a Boolean program model from a
C program [BMMR01], showing also a way to combine effectively model
checking and theorem provers. Automated abstraction is also proposed
by Heitmeyer et al. [HKLAB98] for using SMV to check a weapon control
software system specified in SCR.
Successes of model-checking
have encouraged researchers to extend the idea of model-checking to
infinite-state and real-time systems.
Model-checking
finite-state systems and model-checking infinite-state systems are
closely related areas, but analyzing infinite-state systems is very
different from analyzing finite-state systems, since new decision
procedures are needed and new complexity issues may arise.
As
already pointed out, verification of finite-state systems may suffer
of the state-explosion problem. However, as far as infinite-state
systems are concerned, a more serious problem - decidability - should
be addressed.
For instance, it is well-known (since Minksy) that
it is not possible to verify automatically whether an arithmetic
program with two integer variables is going to halt on all inputs.
Even though semi-decidable decision procedures are sometimes studied
or even implemented (see [HH95]), it seems fundamental for
infinite-state system research, to assess preliminarily what kinds of
infinite-state systems are decidable with respect to a particular
form of properties.
There are many infinite-state models that
have been investigated in the model-checking community, including
timed automata [AD94], pushdown automata [BEM97, EHRS00, FWW97],
counter machines [CJ98,FS00,ISDBK00,ISDBK01] and various queue
machines [AJ96,CF97,IDS01,PP92]. Studying these infinite-state models
may help researchers to develop verification theories and algorithms
concerning real-world applications such as (real-time) programs with
procedure calls,
communication protocols, reactive systems
containing integer variables, etc.
See for instance [DK97 DK99,
DK00].
In particular, a number of verification tools are
available and used for analyzing real-world real-time systems,
usually based on temporal logic and/or timed automata.
Among the
tools for verifying temporal logic specifications, we remind the work
in our group around the TRIO toolkit [MS94] for real-time system
specification, where verification and validation is mainly based on
test case generation [SMM00]. The algorithms used in such toolkit are
based on tableaux methods rather than model-checking, but they could
strongly benefit by the adoption of model checking techniques coupled
with infinite-state timed automata, as discussed next.
Timed
automata are a natural model for real time systems, since they
promise to offer more systematic means to make analysis and design
more reliable.
Timed Automata were originally defined by Alur and
Dill in [AD94], and they have been a subject of great interest and
intense study ever since (see R. Alur, Timed automata, CAV'99,LNCS
1633, pp. 8-22, for a recent survey of current research).
A timed
automaton can be considered as a finite automaton augmented with a
number of dense (either real or rational) clocks. Clocks can be reset
or progress at rate 1 depending upon the truth values of a number of
clock constraints expressed in the form of clock regions (i.e.,
comparisons of a clock or the difference of two clocks against an
integer constant, e.g., x-y>5).
Many properties that
involve simple clock constraints in the form of clock regions can be
verified with the help of the well-known region technique [AD94].
The
region technique, when verifying region constraints, reduces a timed
automaton to a finite-state system, making it possible to use
well-established techniques (such as model-checking) of finite-state
systems.
Tools such as Timed COSPAN [AK96,CDCT92], KRONOS [Y97],
UPPAAL [LPY97] and HyTech [HH95] that implement the region technique
are available and proven practically useful for analyzing some
real-time systems.
However, the region technique is of limited
usefulness for applications with complex, non-region timing
requirements: for instance, the binary reachability cannot be studied
with regions only. Therefore, we wish to exploit different techniques
based on automata and formal languages theory.
The theory of
formal languages had a great development in the 60's and 70's, when
considerable research was done on formal grammars, automata theory,
logic, topology and semigroup theory.
Successful applications of
the theory occurred in the areas of logic/digital circuits,
syntax-directed compilation and language processing, where methods
based on formal language theory are commonly used by hardware and
software designers. The classical results as well as recent additions
to the theory are presented in the opus [RS97].
Recently, these
traditional techniques have been revived by the investigation of
model checking and timed automata. For instance, a LTL model checking
problem can always be regarded as the emptiness of the inclusion of
two languages. In particular, decidability of the emptiness is
particularly relevant for model checking timed automata (see [Y98]).
A recent example of an automata-theoretic approach to verification is
the recent [DSK01] paper which has done a systematic study of
decidability for liveness properties of timed automata, when
Presburger formulas on configurations are allowed.
The
automata-theoretic approach, based on formal language theory, usually
allows much easier and more direct proofs than other approaches, but
it has not been extensively used in model checking.
For instance,
[CJ99, CC00] showed, by using algebraic or graph-oriented techniques,
the decidability of binary reachability for timed automata. However,
the papers are very lengthy and complex and the proofs cannot be
easily generalized to extensions of timed automata.
Instead, the
approach of [D01], based on automata theoretic considerations applied
to dense time models, allows a much easier proof of a much more
general result. The pattern technique introduced in this paper works
for timed automata augmented with other discrete data structures like
a pushdown stack or a restricted queue (such as a half-duplex queue
[CF97]) with asynchronous clocks.
This and other
automata-theoretic works derive from the study of automata augmented
with various kinds of counters, which was pioneered by Greibach
[G75,G78] and Ibarra [I78]. The study of extension of timed automata
with discrete data structures is actuallu very recent, being started
in [DIBKS00], but it seems that it can be continued and extended to
more general structures than pushdown stacks, such as multipushdowns
and multiqueues [CS96, CS00, CCS01]. Notice that approaches other
than automata-theoretic are currently not able to deal with these
extensions when coupled with timing requirements.
In contexts
originally very far from model checking, many
generalizations/restrictions have been proposed on top of
context-free grammars and of pushdown automata. The original aim was
capturing some non-context-free aspects of programming and natural
languages, while preserving the attractive properties of the
classical models, such as polynomial time parsing, or improving the
complexity/decidabily of decision problems.
For such families of
languages typical problems that have been investigated are closure
properties, parsing complexity and generative capacity, as for
instance in the above referenced works on multipushdowns and
multiqueues and on our work on Associative Language Descriptions
[CCS01].
For instance, for the queue automaton model, which may
be traced back to the Post machine, many decidability and complexity
problems are still open, at least for suitable restrictions on the
queue behavior; such problems were for instance partially
investigated in A. Cherubini at al., QRT FIFO Automata, Breadth-first
Grammars and their Relations, Theor.Comp.Sc., 1991, pp. 171-203, in
the case of quasi-real-time automata. An application of queue
automata to operating systems schedulers is described in [BCC99]. The
latter work could be used as a formal basis for verifying and
developing real-time schedulers.
We want to investigate whether
such models are fit for describing interesting software systems, and
to study the decidability and complexity of their verification by
using the tools and techniques of formal language and automata
theory. This may require further theoretical investigation in the
models and in their properties.
Our group has recently
started investigations about application of model checking to static
analysis, with the goal of improving analysis for efficient execution
on the coming generation of ILP processors. In fact, recent advances
in the design of microprocessor architectures have introduced
parallelism at the level of instruction execution (called ILP,
Instruction Level Parallelism).
A challenge for modern compilers
is to parallelize machine code, to allow efficient executions on ILP
processors.
A wide set of code transformations has been studied,
see for instance D. Bacon, S. Graham, O. Sharp, "Compiler
Transformations for High-Performance Computing", in ACM
Computing Surveys, vol. 26, n. 4, pp. 345-419, 1994. These
transformations rely on the possibility of an accurate static
analysis of the program before compilation.
In [MS01], we showed
that, at least in the case of intraprocedural alias analysis, a model
checking tool has a great potential for precision and efficiency. For
instance, we can easily deal, with good precision, with features such
as pointer arithmetic, arrays, structures and dynamic memory
allocation.
The approach for applying model checking to software
programs and specifications is to use some form of abstraction to
reduce the number of states. An abstraction omits many details, such
as data structures, of the system to be checked. Finding the right
abstraction is in general a very difficult problem, and there may be
no guarantee that the verification of the abstracted system brings
any information about the real system. In the case of alias analysis,
however, we are mainly interested in pointer expressions and we can
thus abstract away significant parts of the code to be checked,
without loosing the correctness of the results.
Also, various
conservative approximations may be applied to the original code,
leading to small, and efficiently analyzable, finite state machines,
but still providing a good precision of the analysis. At the very
least, the great flexibility allowed in defining the may-alias
relation, should make it easier to experiment and to examine the
connections among the accuracy of an alias analysis and the
optimizations available in the various compilation phases. Important
contributions may also come from the above-referenced study of
infinite-state model checking, for the importance of dealing with
unbounded data structures such as a stack or a heap.
There is no
previous application of model checker technology to this goal.
However, there are various studies about the application of model
checking to flow analysis, e.g. Steffen [S91]. In this and in similar
works, it has been shown that many problems usually solved by means
of data-flow techniques can be solved more simply by model checking
techniques.
In particular, our work is consistent with the
methodology proposed by Steffen, which uses Cousot's abstract
interpretation to abstract and analyze programs by combining model
checking and data flow techniques.
Trace theory is another model
coming from automata and formal languages that seems to be promising
in reducing the study of ILP compilation to the formal language
models.
Trace theory is a mathematical tool originally defined
for modelling concurrent systems by partially commutative monoids,
(e.g., V. Diekert, G. Rozenberg, "The Book of Traces",
World Scientific, 1995). Its application to ILP compilation seems
useful at least for loop parallelization, one of the most important
code transformations: the link is provided by the standard Foata
normal form of a trace language, which gives a maximally parallel
form of a program schema.
AJ96 P.Abdulla and B.Jonsson.Verifying programs with unreliable channels.Information and Computation, 127(2):91-101, 1996.
AD94 R.Alur and D.L.Dill. A theory of timed automata. Theoretical Comp. Sc., 126(2):183-235, April 1994. AH99 R.Alur and T.A.Henzinger. Reactive modules. Formal Methods in System Design,15(1):7-48, July 1999.
AH97 H.R.Andersen and H.Hulgaard.Boolean expression diagrams. 12th IEEE Symp.on Logic in Comp.Sc., p.88-98, Warsaw, Poland, 29 June-2 July 1997.
AK96 R.Alur and R.P.Kurshan. Timing analysis in cospan. Hybrid Systems III, LNCS 1066, p.220-231.
BCC99 L.Breveglieri, S.Crespi Reghizzi and A.Cherubini, Modelling operating system schedulers with multi-stack-queue grammars, FCT99, LNCS 1684.
BMMR01 T.Ball, R.Majumdar, T.Millstein, and S.K.Rajamani. Automatic predicate abstraction of C programs. In PLDI 2001, ACM SIGPLAN Notices 5(36): 203-213, 2001.
BCCZ99a A.Biere, A.Cimatti, E.Clarke, and Y.Zhu. Symbolic model checking without BDDs. TACAS 1999, LNCS 1579, p.193-207.
BCCZ99b A.Biere, A.Cimatti, E.Clarke, and Y.Zhu. Verifying safety properties of a power pc microprocessor using symbolic model checking without bdds. CAV 1999,LNCS 1633, p.60-71.
BEM97 A.Bouajjani, J.Esparza, and O.Maler. Reachability analysis of pushdown automata: application to model-checking. CONCUR'97, LNCS 1243, p.135-150. Springer, 1997.
B86 R.E.Bryant. Symbolic manipulation of boolean functions using a graphical representation. 22nd ACM/IEEE Design Automation Conf., p.688-694, Los Alamitos, Ca., USA, June 1985.
CF97 G.Cece and A.Finkel. Programs with quasi-stable channels are effectively recognizable. CAV'97, LNCS 1254, p.304-315.
CE81 E.M.Clarke and E.A.Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Workshop of Logic of Programs 1981, LNCS 131.
CES86 E.M.Clarke, E.A.Emerson, and A.P.Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2):244-263, April 1986.
CGL94 E.M.Clarke, O.Grumberg, and D.E.Long. Model checking and abstraction. ACM TOPLAS,16(5):1512-1542, Sept. 1994.
CC00 H.Comon and V.Cortier. Flatness is not a weakness. In Proc.Comp.Sc.Logic, 2000.
CJ98 H.Comon and Y.Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. CAV'98, LNCS 1427, p.268-279.
CJ99 H.Comon and Y.Jurski. Timed automata and the theory of real numbers. CONCUR'99, LNCS 1664, p.242-257.
CS96 A.Cherubini, P.San Pietro, A Polynomial Time Parsing Algorithm for k-depth Languages, J.of Computing and System Science 52 (1), 1996, pp.61-79.
CS00 A.Cherubini, P.San Pietro, Multipushdown Languages and Tree Adjoining Languages, Theory of Computing Systems, vol.33-4, pp 257-293, 2000.
CCS01 A.Cherubini, S.Crespi Reghizzi, P.San Pietro, Associative Language Descriptions, to appear in Theoretical Comp.Sc..
D01 Zhe Dang. Binary reachability analysis of pushdown timed automata with dense clocks. CAV'01, LNCS 2102, p.506-517.
DI01 Zhe Dang and O.H.Ibarra. Liveness Verification of Reversal-bounded Multicounter Machines with a Free Counter. Submitted.
DIBKS00 Zhe Dang, O.H.Ibarra, T.Bultan, R.A.Kemmerer, and J.Su. Binary reachability analysis of discrete pushdown timed automata. CAV'00, LNCS 1855, p.69-84.
DK97 Zhe Dang and R.A.Kemmerer. Using the ASTRAL Model Checker for Cryptographic Protocol Analysis. DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
DK99 Zhe Dang and R.A.Kemmerer. Using the ASTRAL Model Checker to Analyze Mobile IP. In Proc.of the 1999 International Conf.on Softw. Eng. (ICSE'99), p.132-141.
DK00 Zhe Dang and R.A.Kemmerer. Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems. ICSE'00, p.345-354.
DSK01 Zhe Dang, P.San Pietro, and R.A.Kemmerer. On Presburger Liveness of Discrete Timed Automata. In Proc.of the 18th International Symp.on Theoretical Aspects of Comp. Sc. (STACS'01), LNCS 2010, p.132-143.
D89 D.Dill. Timing assumptions and verification of finite state concurrent systems. LNCS 407, p.197-212. Springer, 1989.
EHRS00 J.Esparza, D.Hansel, P.Rossmanith, and S.Schwoon. Efficient algorithms for model checking pushdown systems. CAV'2000, LNCS 1855, p.232-247.
FS00 A.Finkel and G.Sutre. Decidability of reachability problems for classes of two counters automata. STACS'2000, Lille, France, Feb.2000, LNCS 1770, p.346-357.
FWW97 A.Finkel, B.Willems, and P.Wolper. A direct symbolic approach to model checking pushdown systems. INFINITY'97, 1997.
G75 S.A.Greibach. One counter languages and the IRS condition. Journal of Comp. and System Sc., 10(2):237-247, April 1975.
G78 S.A.Greibach. Remarks on blind and partially blind one-way multicounter machines. Theoretical Comp. Sc., 7(3):311-324, Dec. 1978.
GW94 P.Godefroid and P.Wolper. A partial approach to model checking. Information and Computation, 110(2):305-326, 1 May 1994.
GL94 O.Grumberg and D.E.Long. Model checking and modular verification. ACM TOPLAS,16:843-872, 1994.
HKLAB98 C.Heitmeyer, J.Kirby, B.Labaw, M.Archer, and R.Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE TSE, 24(11):927-948,Nov. 1998.
HH95 T.A.Henzinger, P.-H.Ho, and H.Wong-Toi. sc HyTech: A Model Checker for Hybrid Systems. CAV'97, LNCS 1254, p.460-463.
H97 G.J.Holzmann. The model checker SPIN. IEEE TSE, 23(5):279-295, May 1997.
H99 G.J.Holzmann and M.H.Smith. Softw. model checking - extracting verification models from source code. Formal Methods for Protocol Engineering and Distributed Systems, p.481-497, Kluwer Academic Publ., Oct. 1999.
I78 O.H.Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM, 25(1):116-133, Jan. 1978.
IDS01 O.H.Ibarra, Zhe Dang, and P.San Pietro. Verification in loosely synchronous queue-connected discrete timed automata. submitted.
ISDBK00 O.H.Ibarra, J.Su, Zhe Dang, T.Bultan, and R.A.Kemmerer. Counter machines: decidable properties and applications to verification problems. 25th International Symp.on Mathematical Foundations of Comp.Sc.(MFCS 2000), LNCS 1893, p.426-435.
ISDBK01 O.H.Ibarra, J.Su, Zhe Dang, T.Bultan, and R.A.Kemmerer. Counter machines and verification problems. Theoretical Comp.Sc., (to appear).
LPY97 K.G.Larsen, P.Pettersson, and W.Yi. {UPPAAL} in a nutshell. International Journal on Softw. Tools for Technology Transfer, 1(1-2):134-152, 1997.
ND96 C.Norris Ip and David L.Dill. Better verification through symmetry. Formal Methods in System Design, 9(1/2):41-75, August 1996.
M93 K.L.McMillan. Symbolic Model Checking. Kluwer Academic Publ., Norwell, MA, 1993.
MS94 A. Morzenti, P.San Pietro. Object-Oriented Logic Specifications of Time Critical Systems. ACM TOPLAS, Jan. 1994, pp.56-98.
MS99 Marques-Silva and Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans.on Comp., 48(5), 1999.
MS01 V.Martena, P.San Pietro, Alias Analysis by means of a Model Checker, CC2001, Intern. Conf. on Compiler Construction, Genova, Italia, 2-6 April, 2001, LNCS.
PP92 W.Peng and S.Purushothaman. Analysis of a class of communicating finite state machines. Acta Informatica, 29(6/7):499-522, 1992.
P77 A.Pnueli. The temporal logic of programs. FOCS-77, p.46-57, Providence, Rhode Island,31-2, 1977, IEEE.
RS97 G.Rozenberg, Salomaa A. Eds., Handbook ofFormal Languages, Springer-Verlag, 1997.
S91 B.Steffen, Data Flow Analysis as Model Checking. TACS'91, Sendai (Japan), Sep. 1991 , pp.346-365.
SC85 A.P.Sistla and E.M.Clarke. Complexity of propositional temporal logics. Journal of ACM, 32(3):733-749, 1983.
SMM00 P. San Pietro, A.Morzenti, S.Morasca. Generation of Execution Sequences for Modular Time-Critical Systems. IEEE TSE vol. 26 n.2, Feb. 2000, pp. 128-149.
WBCG00 P.F.Williams, A.Biere, E.M.Clarke, and A.Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. CAV'00, LNCS 1855, p.124-138.
First activity: verification of timed automata. Collaborations: WSU, UCSB. Timed automata are suitable for specifying the temporal behaviour of real-time systems. This project will study the decidability and complexity properties of the timed behaviour of such automata, possibly extended with memory structures such as queues and multistacks. We plan to divide this activity in 5 subactivities: 1) calculating the binary reachability of timed automata augmented with a stack or a restricted queue; 2) investigating whether there exists a verifiable fragment of Presburger Linear Temporal logic for timed automata and their extensions, and to better combine existing temporal logic, such as TRIO, with suitable versions of timed automata. 3) studying the verification problem for timed automata augmented with other dense data structures, e.g., dense counters. 4) developing the fundamental theory and verification algorithms for these extended time automata and implement and build these algorithms into a verification library, such as the TRIO toolkit, with the cooperation of WSU. 5) applying the verification library to the composed model for verification through a number of real-time applications.
Second activity: static analysis of programs. Our research unit wants to study the applicability of an automatic-theoretic approach to static analysis, such as liveness analysis and the aliasing of pointers, to be modeled as reachability/model checking problems of suitable finite-state automaton. The main issue is the definition of careful abstractions on C or java programs to make finite state model of the program, and on the use of model checkers. These results will be used to study code transformations for optimization and parallelization of ILP code. As already remarked, a goal of our research is the integration of the resulting analysis toolkit with other less precise analysis tools, such as one being developed in our group in cooperation with HU and CRL. A model checking tool could be used to check only those parts of a program that are found in need of greater optimization and thus require more precision in the analysis. Alternatively, if experiments with the model checker may show that a certain kind of precise analysis is feasible and useful for optimization, specific algorithms and tools will also be developed. Another subactivity concerns trace theory. The intention of our unit is to model the possible scheduling policies applied to machine code, investigating the possible contributions of the theory to loop optimization.
Third activity: formal properties of infinite-state models. Collaborations: WSU, UCSB. Infinite-state models such as queue automata and Associative Language Descriptions are abstract models of the behaviour of concurrent systems and stack systems. This unit wants to investigate both the fundamental properties of these and other models, in particular the decidability and complexity of recognition and verification, and their descriptional power, for instance for modelling operating system schedulers.
In the first two activities, the theoretical investigations will take place in the first and in the second years, while algorithm development and implementation) will be dealt with especially in the third year. Case studies will be developed in the second and third year. Experiments will be already performed starting in the first year. The third activity, lasting only for the first two years, will be only of theoretical investigation, but its results could contribute to drive the other two activities.
Starting Date: February 2003
Ending Date: February 2006
Financial Support: Politecnico di Milano and Miur (FIRB).
O. Ibarra, Z. Dang, P. San Pietro, Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata, Theoretical Computer Science. vol 290 (30 Jan 2003), pp. 1713 –1735. Elsevier Publishing, Amsterdam.
M. Verdicchio, P. San Pietro, Model Checking the Secure Electronic Transaction Protocol, DASD 2003 (Design, Analysis and Simulation of Distributed Systems), Mar 30 – Apr 4, 2003, Orlando, FL, USA.
Z. Dang, P. San Pietro, R. Kemmerer, On Presburger Liveness of Discrete Timed Automata, Theoretical Computer Science, Vol. 299, Issue 1, 18 April 2003, pp. 413-438. Elsevier Publishing, Amsterdam.
Umberto Foschi, Mauro Giuliani, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro: The Role of Formal Methods in Software Procurement for the Railway Transportation Industry, in FORMS 2003: Symposium on Formal Methods for Railway Operation and Control Systems. 15-16 May 2003, Budapest, Hungary.
Gaoyan Xie, Zhe Dang, Oscar Ibarra, and Pierluigi San Pietro, Dense counter machines and verification problems, in CAV03: 15th Computer-Aided Verification Conference. Boulder, Colorado, USA, July 8 -- 12, 2003.
P. San Pietro and Z. Dang, Automatic verification of multi-queue discrete timed automata, in COCOON 03: 9th International Computing and Combinatorics Conference, July 25-28, 2003, Big Sky, MT, USA.
A. Cherubini, S. Crespi Reghizzi, P. San Pietro, Associative Language Descriptions, Theoretical Computer Science, 270, Issue 1-2, 6 January 2002, pp. 463-491.
A. Morzenti, M. Pradella, P. San Pietro, P. Spoletini, Model Checking TRIO specifications in SPIN, in FM 03: Formal Methods Europe Conference, Pisa, September 2003.
A. Morzenti, M. Pradella, P. San Pietro, P. Spoletini, Practical Model Checking of LTL with Past, in ATVA03: 1st Workshop on Automated Technology for Verification and Analysis, Taipei, Taiwan, 2003, p 135-146. 10-13 December 2003.
A. Campi, E. Martinez, P. San Pietro, Experiences with a Formal Method for Design and Automatic Checking of User Interfaces, Position paper in IUI/CADUI'2004 Workshop on Making Model-Based UI Design Practical: usable and open methods and tools, Madeira, Portugal, 13th January, 2004.
M. Verdicchio, P. San Pietro, Model Checking-Aided Design of Secure Distributed Systems, SE 2004: IASTED International Conference on Software Engineering, February 17-19, 2004, Innsbruck, Austria.
Marcella Anselmo, Alessandra Cherubini, Pierluigi San Pietro, Regular Languages and Associative Language Descriptions, in JM2004: Journées Montoises d'Informatique Théorique à Liège, 8-11 Septembre 2004 .
Zhe Dang, Oscar Ibarra, Pierluigi San Pietro, Gaoyan Xie. Real-Counter Automata and Applications to Verification, in FSTTCS 2004, 24th Foundations Of Software Technology And Theoretical Computer Science, December 16--18, 2004, Chennai, India.
J. Berstel, S. Crespi Reghizzi, G. Roussel, P. San Pietro, A scalable formal method for Design and Automatic Checking of User Interfaces, ACM TOSEM, Volume 14, Number 2 (April 2005).
Marcella Anselmo, Alessandra Cherubini, Pierluigi San Pietro, Regular Languages and Associative Language Descriptions, in Journal of Automata, Languages and Computation (to appear).
S. Crespi Reghizzi, M. Pradella, Tile Rewriting Grammars and Picture Languages, Theoretical Computer Science, Vol 340/2 pp 257-272, 2005 (file)
A. Cherubini, S. Crespi Reghizzi, M. Pradella, P. San Pietro, Picture languages: Tiling Systems versus Tile Rewriting Grammars, to appear on Theoretical Computer Science.
The VEG toolkit
The Trio-Spin tool.
The Trident toolkit for editing Trio Specifications.
A parser generator for Associative Language Descriptions,
Financial Support: Politecnico and MIUR (FIRB)