arXiv subjects

Maryam Ghaffari Saadat

Publications and source records attributed to Maryam Ghaffari Saadat.

4 recordsLinked to original sources

arXiv2024

ROSMonitoring 2.0: Extending ROS Runtime Verification to Services and Ordered Topics

Formal verification of robotic applications presents challenges due to their hybrid nature and distributed architecture. This paper introduces ROSMonitoring 2.0, an extension of ROSMonitoring designed to facilitate the monitoring of both topics and services while considering the order in which messages are published and received. The framework has been enhanced to support these novel features for ROS1 -- and partially ROS2 environments -- offering improved real-time support, security, scalability, and interoperability. We discuss the modifications made to accommodate these advancements and present results obtained from a case study involving the runtime monitoring of specific components of a fire-fighting Uncrewed Aerial Vehicle (UAV).

cs.SE↗

arXiv2020

Encoding Incremental NACs in Safe Graph Grammars using Complementation

In modelling complex systems with graph grammars (GGs), it is convenient to restrict the application of rules using attribute constraints and negative application conditions (NACs). However, having both attributes and NACs in GGs renders the behavioural analysis (e.g. unfolding) of such systems more complicated. We address this issue by an approach to encode NACs using a complementation technique. We consider the correctness of our encoding under the assumption that the grammar is safe and NACs are incremental, and outline how this result can be extended to unsafe, attributed grammars.

cs.LO↗

arXiv2020

Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping

Graph transformation theory relies upon the composition of rules to express the effects of sequences of rules. In practice, graphs are often subject to constraints, ruling out many candidates for composed rules. Focusing on the case of sesqui-pushout (SqPO) semantics, we develop a number of alternative strategies for computing compositions, each theoretically and with an implementation via the Python API of the Z3 theorem prover. The strategies comprise a straightforward generate-and-test strategy based on forbidden graph patterns, a variant with a more implicit logical encoding of the negative constraints, and a modular strategy, where the patterns are decomposed as forbidden relation patterns. For a toy model of polymer formation in organic chemistry, we compare the performance of the three strategies in terms of execution times and memory consumption.

cs.LO↗

arXiv2019

Analysis of Graph Transformation Systems: Native vs Translation-based Techniques

The paper summarises the contributions in a session at GCM 2019 presenting and discussing the use of native and translation-based solutions to common analysis problems for Graph Transformation Systems (GTSs). In addition to a comparison of native and translation-based techniques in this area, we explore design choices for the latter, s.a. choice of logic and encoding method, which have a considerable impact on the overall quality and complexity of the analysis. We substantiate our arguments by citing literature on application of theorem provers, model checkers, and SAT/SMT solver in GTSs, and conclude with a general discussion from a software engineering perspective, including comments from the workshop participants, and recommendations on how to investigate important design choices in the future.

cs.SE↗