Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Powiadomienia systemowe

Sesja wygasła!
Sesja wygasła!

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Formal Analysis of SystemC Designs in Process Algebra

Hojjat H., Mousavi M. R., Sirjani M.

Fundamenta Informaticae

2011

Vol. 107, nr 1

19-42

SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.

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.