Cílem této diplomové práce je analýza marketingové strategie společnosti REBECA mode s.r.o. a stanovení vhodných doporučení na základě dotazníkového výzkumu. V první části jsou shrnuta základní teoretická východiska marketingové strategie, v dalších kapitolách následují charakteristika společnosti REBECA mode s.r.o. a analýza její současné marketingové strategie. Na závěr jsou prezentovány výsledky dotazníkového výzkumu, na jejichž základě byla stanovena doporučení pro zefektivnění marketingové strategie dané společnosti.

Unified Modeling Language (UML) is recognized as a de facto standard for modeling various typesof systems. However, its lack of formal semantics hinders the ability to perform formal verification, which is crucial to ensure the correctness of the models throughout the modeling process. Rebeca isan actor-based modeling language designed to formally verify reactive concurrent systems. Previous work has attempted to bridge the gap and provide a translation to take advantage of both UML and Rebeca’s benefits. These methods either require multiple UML diagrams and an understanding of Rebeca, or lack implementation solutions. We conducted experiments to explore the potential of zero-shot and few-shot learning with ChatGPT-4 as a tool for automating the translation from UML state diagrams to Rebeca code. The results indicated that the translation from UML state diagrams to Rebeca code can be partially made and they are not sufficient to derive correct Rebeca models. To mitigate this, we augment state diagrams with metadata, which resulted in the generated code having minor errors and requiring slight adjustments to be able to be compiled in the Rebeca model checking tool, Afra. The conclusion is that ChatGPT-4 can potentially facilitate the process of transforming UML state diagrams into executable Rebeca code with minimal additional information. We provide a translation procedure of Rebeca code to UML state diagrams, a conceptual mapping of them in reverse, and a dataset that can be used for further research. The dataset and the results are published in the GitHub repositoryof our project

Cyber-physical systems (CPSs) are used in several industries, such as healthcare, automotive, manufacturing, and more. The fact that CPSs often contain components integrated via communication networks means that malicious actors can exploit vulnerabilities in these components through cyber attacks. CRYSTAL Framework has been shown in previous research to be able to detect cyber attacks on CPSs. However, this has only been proven in simulation. Our research builds upon these previous research as we aim to prove that CRYSTAL Framework is a viable method for monitoring real systems to detect abnormal behaviours.  The Tiny Twin is an abstract behavioral model that defines normal running behaviour of a system, which can then be used by to compare the current state of a monitored system to detect possible attacks and abnormal behaviours. We built a monitor that integrates such a Tiny Twin, working by passively listening on input and output of components in a monitored system. We designed and implemented two different scenarios, a security alarm system and a temperature control system (TCS), to test the CRYSTAL Framework. In testing both implemented scenarios our monitor successfully detected all but one attacks during runtime by comparing the system's current state with the expected state as defined in the Tiny Twin.

Unified Modeling Language (UML) is a de-facto standard modeling language with an extensive syntax and notations that can be used to model systems of any kind. However, being a general-purpose language, its semantics are intrinsically under-specified and broad to leave a room for different interpretations. This, in general, hinders the ability to perform formal verification of models produced with a specific domain in mind. In these cases, it is usually more suitable to map the UML models to other domains, where modeling concepts have stricter semantics. Notably, Reactive Objects Language (Rebeca) is an actor-based language with a formal foundation and formal verification support. This paper aims to identify a subset of UML modeling concepts compatible with the domain of reactive and distributed systems as modeled in Rebeca. In this respect, this work proposes a conceptual mapping between a sub-portion of UML and Rebeca, with the goal of enabling formal verification early in the design process. In particular, we investigate Rebeca syntax, and for each Rebeca concept, we provide the corresponding concept in the UML, as part of an iterative process. This process ends when all Rebeca concepts are exhausted and comprehensive mapping procedure emerges. Additionally, validation is an important part of this paper as it aims to establish confidence in the developed mapping procedure (in post-conversion validation) and avoid doing the transformation if the design is not compatible with the mapping procedure (in pre-conversion validation). As part of the pre-conversion validation, in order to establish the compatibility with the mapping procedure, we provide an extensive list of correctness attributes. As part of the post-conversion validation, the mapping procedure is validated by transformation on the provided examples. The results of this transformation show the wide range applicability of the mapping procedure and serve as an assertion of its comprehensiveness.

Security is widely recognized as an important property that is tightly interdependentwith safety in safety-critical systems. The goal of this thesis is to conduct case studies on the implications that security attacks may have on the safety of these systems.In these case studies, we formally model the design of a robot arm system, verify itssecurity against some potential attack scenarios, propose mitigation techniques andanalyze their effectiveness. In order to achieve a thorough knowledge about the current formal verification approaches and select a proper modeling language/tool, weconducted an extensive literature review. We performed this review following a wellknown approach proposed by Barbara Kitchenham. The procedure and outcomes ofthis review are detailed in this thesis. Based on the literature review, we chose TRebeca, (a timed extension of Rebeca), as the formal language to model the robot armsystem, attack scenarios and mitigation techniques. Rebeca is an actor-based modeling language with a Java-like syntax that is effectively used to model concurrent anddistributed systems. This language is supported by a full-featured IDE called Afra,which facilitates the development of (T)Rebeca models and verification of correctnessproperties (such as safety and security) on them. Among several functions providedby a robot arm system, we chose two important functions i.e., Stand Still Supervisionand Control Error Supervision, which we believe would be interesting for attackerstrying to get control over robot movements. In particular, attackers may maliciouslymanipulate the parameter values of these functions, which may lead to safety issues.In order to find suitable attack scenarios on these functions, we studied the mostimportant security protocols used in safety-critical industrial control systems. Weobserved that these systems are vulnerable to several attacks, and man-in-the-middleattack is among the most successful attacks on these systems. Based on this study,we devised two attack scenarios for each function and modeled them with TRebeca.To mitigate these attacks, we proposed a redundancy technique, whose effectivenesswas also assured by Afra.

Thesis (Ph. D.)--University of Notre Dame, 2008. / Thesis directed by María Rosa Olivera-Williams for the Department of Romance Languages and Literatures. "March 2008." Includes bibliographical references (leaves 206-215).

ROS2 is an increasingly popular middleware framework for developing robotic applications. A ROS2 applicationbasically is composed of nodes that run concurrently and can be deployed distributedly. ROS2 nodes communicatewith each other through asynchronous interfaces; they reside in memory and wait to respond events that circulatearound the system during the interactions between the robot(s) and the environment. Rebeca is an actor-basedlanguage for modelling asynchronous, concurrent applications. Timed Rebeca added timing features to Rebeca todeal with timing requirements of real-time systems. The similarities in the concurrency and message-basedasynchronous interactions ofreactive nodes justify the relevance of using Timed Rebeca to assist the developmentand verification of ROS2 applications. Model-based development and model checking allow quicker prototypingand earlier detection ofsystem errors without the requirement of developing the entire real system. However, thereare challenges in bridging the gaps between continuous behaviours in a real robotic system and discrete behavioursin a model, between complex computations in a robotic system and the inequivalent programming facilities in amodelling language. There have been previous attempts in mapping Rebeca to ROS, however they could not beput into practice due to over-simplifications or improper modelling approaches. This thesis addresses the problemfrom a more systematic perspective and has been successful in modelling a realistic multiple autonomous mobilerobots system, creating corresponding ROS2 demonstration code, showing the synchronization between the modeland the program to prove the values of the model in driving development and automatic verification of correctnessproperties (freedom ofdeadlocks, collisions, and congestions). Stability of model checking results confirms designproblems that are not always detected by simulation. The modelling principles, modelling and implementingtechniques that are invented and summarized in this work can be reused for many other cases.