Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

4 Fundamenta Informaticae

Znaleziono wyników: 4

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Timed Automata with non-Instantaneous Actions

100%

Barbuti R. , De Francesco N. , Tesei L.

Fundamenta Informaticae

2001

tom Vol. 47, nr 3,4

189-200

In this paper we propose a model, timed automata with non-instantaneous actions, which allows representing in a suitable way real-time systems. Timed automata with non-instantaneous actions extend the timed automata model by dropping the assumption that actions are instantaneous: in our model an action can take some time to be completed. We investigate the expressiveness of the new model, comparing it with classical timed automata. In particular, we study the set of timed languages which can be accepted by timed automata with non-instantaneous actions. We prove that timed automata with non-instantaneous actions are more expressive than timed automata and less expressive than timed automata with e edges. Moreover we define the parallel composition of timed automata with non-instantaneous actions. We point out how the specification by means of a parallel timed automaton with non-instantaneous actions is, in some cases, more convenient to represent reality.

Concrete and Abstract Semantics to Check Secure Information Flow in Concurrent Programs

100%

Bernardeschi C. , De Francesco N. , Lettieri G.

Fundamenta Informaticae

2004

tom Vol. 60, nr 1-4

81--98

This paper presents a technique for verifying secure information flow in concurrent programs consisting of a number of independently executing sequential processes with private memory. Communications between processes are synchronous. Moreover, processes are open systems that can accept inputs from the environment and produce outputs towards the environment. The technique is based on an abstract interpretation. First we define a concrete instrumented semantics where each value is annotated with the security level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level.

A Notion of Non-Interference for Timed Automata

100%

Barbuti R. , De Francesco N. , Santone A. , Tesei L.

Fundamenta Informaticae

2002

tom Vol. 51, nr 1,2

1-11

The non-interference property of concurrent systems is a security property concerning the flow of information among different levels of security of the system. In this paper we introduce a notion of timed non-interference for real-time systems specified by timed automata. The notion is presented using an automata based approach and then it is characterized also by operations and equivalence between timed languages. The definition is applied to an example of a time-critical system modeling a simplified control of an airplane.

Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems

100%

De Francesco N. , Santone A. , Tesei L.

Fundamenta Informaticae

2003

tom Vol. 54, nr 2,3

195-211

We propose a method to check secure information flow in concurrent programs with synchronization. The method is based on the combination of abstract interpretation and model checking: by abstract interpretation we build a finite representation (transition system) of the behavior of the program. Then we model check the the abstract transition system with respect to the security properties, expressed by a set of temporal logic formulae. The approach allows certifying more programs than previous methods do. The main point is that we are able to check more carefully the scope of indirect information flows.