1,721,103 research outputs found
Timed automata with urgent transitions
No full textIn this paper we propose an extension to the formalism of timed automata by allowing urgent transitions. An urgent transition is a transition which must be taken within a fixed time interval from its enabling time and it has higher priority than other non-urgent transitions enabled in the same state. We give a set of rules formally describing the behavior of urgent transitions and we show that, from a language theoretic point of view, the addition of urgency does not improve the expressive power of timed automata. From a specification point of view, the use of urgent transitions allows shorter and clear specifications of behaviors involving urgency and priority. We use timed automata with urgent transitions for specifying a multicast protocol for mobile computing
Timed automata with urgent transitions
No full textIn this paper we propose an extension to the formalism of timed automata by
allowing urgent transitions. A urgent transition is a transition which must be taken
within a fixed time interval from its enabling time. We give a set of rules formally
describing the behaviour of urgent transitions and we show that, from a language
theoretic point of view, the addition of urgency does not improve the expressive
power of timed automata. However, from a specification point of view, the use of
urgent transitions is crucial, especially in modular specification of systems
A Decidable Notion of Timed Non-Interference
No full textWe present a notion of non-interference which embodies the notion of time. It is useful to verify the strength of a system against attacks depending on the frequency of certain actions. In particular we give a decidable definition of non-interference which can be checked by using existing verification tools. We show an application example of our notion of non-interference by defining a variant of the classical Fischer's mutual exclusion protocol and by analyzing its strength against attacks
Extending the Calculus of Looping Sequences to Model Protein Interaction at the Domain Level
No full textAn Abstract Interpretation Approach for Enhancing the Java Bytecode Verifier
No full textThe Java virtual machine embodies a verifier that performs a set of checks on Java bytecode programs before their execution. The verifier carries out an efficient data-flow analysis applied to a type-level abstract interpretation of the code. The implementations of the bytecode verifier presented a significant problem with programs compiled with the Sun Java compiler (until version 1.4.1): there were legal Java programs which were correctly compiled into a bytecode that was rejected by the verifier. The problem was fixed by removing, in version 1.4.2 and following, some interesting features in the compilation of the try-finally Java construct. Because removing such features has a cost in terms of memory space, in this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the space efficiency of the previous versions of the compiler. We define an abstract interpretation framework in which we model the enhanced version of the verifier. The defined abstract interpretation framework can be considered a good basis for other static analyses of bytecode programs
- …
