Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Uppaal

Sortuj według:

Ogranicz wyniki do:

A Development Methodology for Cyber-Physical Systems based on Deterministic Theatre with Hybrid Actors

Cicirello Franco, Nigro Libero

TASK Quarterly : scientific bulletin of Academic Computer Centre in Gdansk

2021

Vol. 25, No 2

233--260

The goal of the work described in this paper is to propose a development approach for cyber-physical systems (CPS) which relies on actors as the fundamental modelling blocks. The approach is characterized by its capability to deal with the discrete aspects of the cyber part of a CPS, as well as the continuous behaviour of the physical part. More in particular, the approach is based on the Theatre actor system which fosters determinism in model behaviour, and favours model continuity when switching from system modelling and analysis down to prototype and synthesis phases. A key factor of Theatre is the possibility to combine both discrete-event actors, which operate on a discrete timeline, with continuous-time actors which reproduce, in general by using Ordinary Differential Equations (ODEs), the dynamical evolution of physical components. For formal property assessment, Theatre actors (both discrete and continuous) can be reduced to Timed Automata (TA) in the context of the Uppaal toolbox, where the exhaustive andór the statistical model checkers can be exploited. This paper first describes the proposed approach, then it demonstrates its suitability to CPS modelling and analysis through examples. The paper also discusses how abstract and formal modelling actor concepts can be naturally transitioned to implementation concepts in Java.

More flexible models using a new version of the translator of Java sources to timed automatons J2TADD

Rataj A.

Theoretical and Applied Informatics

2009

Vol. 21, No. 2

107-114

Several extensions to the translator J2TADD of Java source code to timed automatons with discrete data are discussed. The changes include support for arrays, reference comparisons, abstract classes and methods, interfaces, the instanceof operator and the so–called experiments. Also, more types of statements can be interpreted.

W artykule omawiane jest kilka rozszerzeń w nowej wersji translatora źródeł Javy do automatów czasowych, J2TADD. Zmiany te to między innymi możliwość używania tablic, porównań referencji, abstrakcyjnych klas i metod, interfejsów, operatora instanceof oraz porównań referencji obiektów. Możliwe jest również opisywanie tak zwanych eksperymentów. Nowa wersja J2TADD umożliwia definiowanie bardziej elastycznych modeli z użyciem bardziej klarownego kodu źródłowego.