Wyniki wyszukiwania - BazTech

1

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

EN

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.

2

Specificity of artistic chronotope in Czech Cubists architecture

Okhrim K.

Przestrzeń i Forma

|

2016

|

nr 27

245--254

EN

Starting from 1910 during two decades phenomena of Cubism was observed in Czech architecture. Irrespective of being so succinct, it was of great importance for the whole process of modernists architecture incipience. Questions from the architectural theory realm are considered in this article, devoted to phenomena of Cubism in Czech architecture in the context of artistic chronotope disquisition.

PL

Zjawisko kubizmu w czeskiej architekturze obserwowano w ciągu dwóch dekad, począwszy od 1910 roku. Będąc tak nietrwałym, jednak miało wielkie znaczenie dla ogólnego procesu rozwoju architektury modernistycznej. W artykule są poddane dyskusji pytania z dziedziny teorii architektury, poświęcone eksploracji fenomenu architektury kubizmu czeskiego w kontekście badań artystycznej czasoprzestrzeni.

3

SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties

Woźna-Szcześniak B., Szcześniak I.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2015

|

Vol. 20

69--81

EN

We define an SAT-based bounded model checking (BMC) method for RTECTLK (the existential fragment of the real-time computation tree logic with knowledge) that is interpreted over timed models generated by timed interpreted systems. Specifically, we translate the model checking problem for RTECTLK to the model checking problem for a variant of branching temporal logic (called EyCTLK) interpreted over an abstract model, and we redefine an SAT-based BMC technique for EyCTLK.

4

Czasowy model bloku przetwarzania danych w systemie pomiarowym

Bilski P., Łukaszewski Ł.

Pomiary Automatyka Kontrola

|

2007

|

R. 53, nr 9 bis

253--256

PL

Artykuł dotyczy modelowania komputerowych systemów pomiarowo-sterujących (KSPS) uwzględniającej czasowe aspekty przepływu informacji w KSPS. W artykule zamieszczono opis części większych prac dotyczących nowej metody opisu modelu KSPS z wykorzystaniem sieci Petri`ego i narzędzia CPN Tools. Szczegółowo przedstawiono model bloku przetwarzania KSPS. Opisano dokładnie funkcje opóźnień zaimplementowane w modelu oraz metodą ich wyznaczania. Dodatkowo zamieszczono badania opóźnień bloku przetwarzania rzeczywistego KSPS oraz symulacje weryfikujące zaprojektowany model.

EN

The paper presents the method of the distributed measuring and control systems modelling, regarding the time aspects of the information flow inside the system. Results of the work including a new method of the measuring system model description using the Petri nets and CPN Tools are included. The data processing model inside the measuring system was presented in detail with delay functions implemented in the model. The paper is concluded with experimental results, comparing simulations with real measuring system behavior.