Wyniki wyszukiwania - BazTech

Ograniczanie wyników

4 Fundamenta Informaticae

Powiadomienia systemowe

Sesja wygasła!
Sesja wygasła!
Sesja wygasła!
Sesja wygasła!

Znaleziono wyników: 4

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

A Petri Net Based Modeling of Active Objects and Futures

de Boer F. S., Bravetti M., Lee M. D., Zavattaro G.

Fundamenta Informaticae

2018

Vol. 159, nr 3

197--256

We give two different notions of deadlock for systems based on active objects and futures. One is based on blocked objects and conforms with the classical definition of deadlock by Coffman, Jr. et al. The other one is an extended notion of deadlock based on blocked processes which is more general than the classical one. We introduce a technique to prove deadlock freedom of systems of active objects. To check deadlock freedom an abstract version of the program is translated into Petri nets. Extended deadlocks, and then also classical deadlock, can be detected via checking reachability of a distinct marking. Absence of deadlocks in the Petri net constitutes deadlock freedom of the concrete system.

A Deductive Proof System for Multithreaded Java with Exceptions

Ábrahám E., de Boer F.S., de Roever W-P., Steffen M.

Fundamenta Informaticae

2008

Vol. 82, nr 4

391-463

Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. Besides that, the language offers a flexible exception mechanism for handling errors or exceptional program conditions. To reason about safety-properties of Java-programs and extending previous work on the proof theory for monitor synchronization, we introduce in this paper an assertional proof method for JavaMT ("Multi-Threaded Java"), a small concurrent sublanguage of Java, covering concurrency and especially exception handling. We show soundness and relative completeness of the proof method.

Modeling and Verification of Reactive Systems using Rebeca

Sirjani M., Movaghar A., Shali A., de Boer F. S.

Fundamenta Informaticae

2004

Vol. 63, nr 4

385--410

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their correctness. In this paper, we develop an actor-based model for describing such systems, use temporal logic to specify properties of the model, and apply different abstraction and verification methods for verifying that the model meets its specification. We use a compositional verification approach for verifying safety properties of these models. For that we introduce a notion of component, based on an user-defined decomposition of the model. Components are more abstract than the model itself, and so we can reduce the state space of the model which makes it more amenable to model checking techniques. We prove that our abstraction technique preserves a set of behavioral specifications in temporal logic. The soundness of the abstraction is proved by the weak simulation relation between the constructs.

A Timed Linda Language and its Denotational Semantics

de Boer F. S., Gabbrielli M., Meo M. C.

Fundamenta Informaticae

2004

Vol. 63, nr 4

309--330

We introduce a Timed Linda language (T-Linda) which is obtained by a natural timed interpretation of the usual constructs of the Linda model and by adding a simple primitive which allows one to specify time-outs. Parallel execution of processes follows the scheduling policy of interleaving, however maximal parallelism is assumed for actions depending on time. We first define the operational semantics of T-Linda by means of a transition system, then we define a denotational model which is based on timed reactive sequences. The correctness of this model is proved w.r.t. a notion of observables which includes finite traces of actions and input/output pairs.