In our previous work, we proposed a verification framework that shifts from the “code is law” to a new “specification is law” paradigm related to the safe evolution of smart contracts. The framework proposed there relaxed the well-established …
verfasst von:
Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, A. W. Roscoe, Filipe Arruda
When creating a software model, it is necessary that it accurately captures the desired behaviour, while at the same time ensuring that any undesired behaviour is excluded. On the one hand, formal verification tools can be used to check the …
The design of cyber-physical systems (CPS) is challenging due to the heterogeneity of software and hardware components that operate in uncertain environments (e.g., fluctuating workloads), hence they are prone to performance issues. Software …
verfasst von:
Riccardo Pinciroli, Connie U. Smith, Catia Trubiani
Over the past few years, several software companies have emerged that offer process mining tools to assist enterprises in gaining insights into their process executions. However, the effective application of process mining technologies depends on …
As neural networks are increasingly being integrated into mission-critical systems, it is becoming crucial to ensure that they meet various safety and liveness requirements. Toward, that end, numerous complete and sound verification techniques …
DEPS (design problem specification) is a new modeling language designed to pose and solve system design problems. DEPS addresses problems of sizing, configuration, resource allocation and of architecture generation for systems. Unlike system …
Model-based engineering emerged as an approach to tackle the complexity of current system development. In particular, compositional strategies assume that systems can be built from reusable and loosely coupled units. However, it is still a …
verfasst von:
Flávia Falcão, Lucas Lima, Augusto Sampaio, Pedro Antonino
The verification of model transformations is important for realizing robust model-driven engineering technologies and quality-assured automation. Many approaches for checking properties of model transformations have been proposed. Most of them …
verfasst von:
Bentley James Oakes, Javier Troya, Jessie Galasso, Manuel Wimmer
Belief–desire–intention (BDI) agents are a popular agent architecture. We extend conceptual agent notation (Can)—a BDI programming language with advanced features such as failure recovery and declarative goals—to include probabilistic action …
Developing robotic applications with human–robot interaction for the service sector raises a plethora of challenges. In these settings, human behavior is essentially unconstrained as they can stray from the plan in numerous ways, constituting a …
verfasst von:
Livia Lestingi, Andrea Manglaviti, Davide Marinaro, Luca Marinello, Mehrnoosh Askarpour, Marcello M. Bersani, Matteo Rossi
Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past (LTL+P ) led to the identification of fragments with lower complexities …
In model checking, when a model fails to satisfy the desired specification, a typical model checker provides a counterexample that illustrates how the violation occurs. In general, there exist many diverse counterexamples that exhibit distinct …