arXiv subjects

Diego Marmsoler

Publications and source records attributed to Diego Marmsoler.

8 recordsLinked to original sources

arXiv2026

Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL

This report presents mechanized query-bounded soundness for a STARK-style protocol in Isabelle/HOL. An acceptance-preserving embedding connects adaptive, privately randomized Fiat-Shamir transcript producers to an established staged adversary experiment and the original probabilistic verifier. The proof combines FRI correlated-agreement reasoning, Merkle authentication, exact modulo-sampler accounting and weighted-path amplification. Event-sensitive accounting refines the complete error bound without changing the verifier or treating repeated oracle calls as free. For a certified 192-bit prime field, trace length 1024 and 640 query repetitions, the concrete theorem bounds false-endpoint acceptance by $2^{-137}$ for every modeled producer satisfying the uniform syntactic oracle-call bound fs_query_bound $(2^{20})$ P. A separate honest-completeness theorem gives acceptance one for the correct square-sequence endpoint in the same final verifier. These are fixed-statement results in a classical, field-valued random-oracle model with terminating finite-support computation, not an unrestricted 137-bit work-factor guarantee. The development does not prove zero knowledge, knowledge extraction, quantum-query security or correctness of a deployed bit-hash implementation. This report retains earlier proof routes as research history; the accompanying current-results overview and checked theorem manifest identify the principal claims and their assumptions.

cs.LO↗

arXiv2023

Modeling Adaptive Self-healing Systems

Motivation: Smart grids design requires energy distribution operations to be adaptable to abnormality. This requirement entails distribution system operators (DSOs) to optimize restoration to normal operational states dynamically. However, these design challenges demand collaborative research efforts on sophisticated modeling and simulation approaches. Approach: In the ESOSEG research project, analyzing the smart grid domain as a software-intensive system, we employed a dynamic architecture approach, particularly the FOCUS theory, to model and assure the domains' self-healing requirements. Although some works specify various self-healing systems, to the best of our knowledge, the use of the approach in smart grids is the first work to enable a formal specification and verification of self-healing properties in smart grids. Results: As a result, to support the modeling and verification process, we developed tool support with Eclipse Modeling Framework (EMF), Xtext, and other languages in the EMF ecosystem. The tool includes a grammar or a meta-model of the DSL, an interface to enable textual and graphical modeling of architectural patterns and code transformer engine for verification. Furthermore, we evaluated the modeling and verification features of the tool support with an e-Car charging scenario for modeling adaptive self-healing properties. Futureworks: As an outlook, future works could include investigation of comprehensive case studies. These, for instance, could be further particular adaptability scenarios addressing challenges in DSOs. Another interesting aspect could be the evaluation of the modeling approach by investigating its use with engineers involved in a smart grid design. Next, the evaluation could be followed with abstractions of the verification process to make it useable by system architects with no knowledge of the proof language, Isabelle/HOL.

cs.SE↗

arXiv2020

Formal Methods in Dependable Systems Engineering: A Survey of Professionals from Europe and North America

Context: Formal methods (FMs) have been around for a while, still being unclear how to leverage their benefits, overcome their challenges, and set new directions for their improvement towards a more successful transfer into practice. Objective: We study the use of formal methods in mission-critical software domains, examining industrial and academic views. Method: We perform a cross-sectional on-line survey. Results: Our results indicate an increased intent to apply FMs in industry, suggesting a positively perceived usefulness. But the results also indicate a negatively perceived ease of use. Scalability, skills, and education seem to be among the key challenges to support this intent. Conclusions: We present the largest study of this kind so far (N = 216), and our observations provide valuable insights, highlighting directions for future theoretical and empirical research of formal methods. Our findings are strongly coherent with earlier observations by Austin and Parkin (1993).

cs.SE↗

arXiv2019

Detecting Architectural Erosion using Runtime Verification

The architecture of a system captures important design decisions for the system. Over time, changes in a system's implementation may lead to violations of specific design decisions. This problem is common in industry and known as architectural erosion. Since it may have severe consequences on the quality of a system, research has focused on the development of tools and techniques to address the presented problem. As of today, most of the approaches to detect architectural erosion employ static analysis techniques. While these techniques are well-suited for the analysis of static architectures, they reach their limit when it comes to dynamic architectures. Thus, in this paper, we propose an alternative approach based on runtime verification. To this end, we propose a systematic way to translate a formal specification of architectural constraints to monitors, which can be used to detect violations of these constraints. The approach is implemented in Eclipse/EMF, demonstrated through a running example, and evaluated using two case studies.

cs.SE↗

arXiv2019

APML: An Architecture Proof Modeling Language

To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former is done using Model Checking, while this does not seem to be the case in general the latter is done using interactive theorem proving (ITP). As of today, however, architects are usually not trained in using a full-fledged interactive theorem prover. Thus, to bridge the gap between ITP and the architecture domain, we developed APML: an architecture proof modeling language. APML allows one to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. With this paper, we introduce APML: We describe the language, show its soundness and completeness for the verification of architecture contracts, and provide an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover Isabelle. Moreover, we describe its implementation in terms of an Eclipse/EMF modeling application, demonstrate it by means of a running example, and evaluate it in terms of a larger case study. Although our results are promising, the case study also reveals some limitations, which lead to new directions for future work.

cs.SE↗

arXiv2017

Verifying Patterns of Dynamic Architectures using Model Checking

Architecture patterns capture architectural design experience and provide abstract solutions to recurring architectural design problems. They consist of a description of component types and restrict component connection and activation. Therefore, they guarantee some desired properties for architectures employing the pattern. Unfortunately, most documented patterns do not provide a formal guarantee of whether their specification indeed leads to the desired guarantee. Failure in doing so, however, might lead to wrong architectures, i.e., architectures wrongly supposed to show certain desired properties. Since architectures, in general, have a high impact on the quality of the resulting system and architectural flaws are only difficult, if not to say impossible, to repair, this may lead to badly reparable quality issues in the resulting system. To address this problem, we propose an approach based on model checking to verify pattern specifications w.r.t. their guarantees. In the following we apply the approach to three well-known patterns for dynamic architectures: the Singleton, the Model-View-Controller, and the Broker pattern. Thereby, we discovered ambiguities and missing constraints for all three specifications. Thus, we conclude that verifying patterns of dynamic architectures using model checking is feasible and useful to discover ambiguities and flaws in pattern specifications.

cs.SE↗

arXiv2017

On the Specification of Constraints for Dynamic Architectures

In dynamic architectures, component activation and connections between components may vary over time. With the emergence of mobile computing such architectures became increasingly important and several techniques emerged to support in their specification. These techniques usually allow for the specification of concrete architecture instances. Sometimes, however, it is desired to focus on the specification of constraints, rather than concrete architectures. Especially specifications of architecture patterns usually focus on a few, important constraints, leaving out the details of the concrete architecture implementing the pattern. With this article we introduce an approach to specify such constraints for dynamic architectures. To this end, we introduce the notion of configuration traces as an abstract model for dynamic architectures. Then, we introduce the notion of configuration trace assertions as a formal language based on linear temporal logic to specify constraints for such architectures. In addition, we also introduce the notion of configuration diagrams to specify interfaces and certain common activation and connection constraints in one single, graphical notation. The approach is well-suited to specify patterns for dynamic architectures and verify them by means of formal analyses. This is demonstrated by applying the approach to specify and verify the Blackboard pattern for dynamic architectures.

cs.SE↗

arXiv2015

A Model of Layered Architectures

Architectural styles and patterns play an important role in software engineering. One of the most known ones is the layered architecture style. However, this style is usually only stated informally, which may cause problems such as ambiguity, wrong conclusions, and difficulty when checking the conformance of a system to the style. We address these problems by providing a formal, denotational semantics of the layered architecture style. Mainly, we present a sufficiently abstract and rigorous description of layered architectures. Loosely speaking, a layered architecture consists of a hierarchy of layers, in which services communicate via ports. A layer is modeled as a relation between used and provided services, and layer composition is defined by means of relational composition. Furthermore, we provide a formal definition for the notions of syntactic and semantic dependency between the layers. We show that these dependencies are not comparable in general. Moreover, we identify sufficient conditions under which, in an intuitive sense which we make precise in our treatment, the semantic dependency implies, is implied by, or even coincides with the reflexive-transitive closure of the syntactic dependency. Our results provide a technology-independent characterization of the layered architecture style, which may be used by software architects to ensure that a system is indeed built according to that style.

cs.SE↗