arXiv subjects

Carlo Ghezzi

Publications and source records attributed to Carlo Ghezzi.

15 recordsLinked to original sources

arXiv2026

Syntax-driven Incremental Program Verification of Matching Logic Properties

Incrementality is a fundamental design principle to master the complexity of large, long-lived software systems. This principle has been embraced by agile development processes and it lays at the base of continuous software evolution. A major challenge in this context is to incrementally re-verify the correctness of software artifacts after every change, focusing the verification efforts only on the parts affected by the change. We present an approach to the incremental verification of programs written in KernelC, annotated with properties expressed in matching logic. The approach is based on a syntactic-semantic framework that enables analyzing code chunks in isolation so that, after a change to a program fragment, only the part whose semantics is affected by the change is re-processed. This property is obtained by expressing the language syntax through an operator precedence grammar and by formalizing its semantics through a synthesized attribute schema. We have implemented our technique in a prototype tool and experimentally evaluated its effectiveness. The results show that our approach does not penalize the efficiency of formal verification and can outperform program re-verification after changes, depending on the presence and type of annotations, as well as the position of the change and the program structure.

cs.SE↗

arXiv2020

Early Validation of Cyber-Physical Space Systems via Multi-Concerns Integration

Cyber-physical space systems are engineered systems operating within physical space with design requirements that depend on space, e.g., regarding location or movement behavior. They are built from and depend upon the seamless integration of computation and physical components. Typical examples include systems where software-driven agents such as mobile robots explore space and perform actions to complete particular missions. Design of such a system often depends on multiple concerns expressed by different stakeholders, capturing different aspects of the system. We propose a model-driven approach supporting (a) separation of concerns during design, (b) systematic and semi-automatic integration of separately modeled concerns, and finally (c) early validation via statistical model checking. We evaluate our approach over two different case studies of cyber-physical space systems.

cs.SE↗

arXiv2020

Cloud Deployment Tradeoffs for the Analysis of Spatially-Distributed Systems of Internet-of-Things

Internet-enabled things and devices operating in the physical world are increasingly integrated in modern distributed systems, supporting functionalities that require assurances that certain critical requirements are satisfied by the overall system. We focus here on spatially-distributed Internet-of-Things systems such as smart environments, where the dynamics of spatial distribution of entities in the system is crucial to requirements satisfaction. Analysis techniques need to be in place while systems operate to ensure that requirements are fulfilled. This may be achieved by keeping a model of the system at runtime, monitoring events that lead to changes in the spatial environment, and performing analysis. This computationally-intensive runtime assurance method cannot be supported by resource-constrained devices that populate the space and must be offloaded to the cloud. However, challenges arise regarding resource allocation and cost, especially when the workload is unknown at the system's design time. As such, it may be difficult or even impossible to guarantee application service level agreements, e.g., on response times. To this end, we instantiate spatial verification processes, integrating them to the service layer of an IoT-cloud architecture based on microservices. We propose several cloud deployments for such an architecture for assurance of spatial requirements -- based on virtual machines, containers, and the recent Functions-as-a-Service paradigm. Then, we assess deployments' tradeoffs in terms of elasticity, performance and cost by using a workload scenario from a known dataset of taxis roaming in Beijing. We argue that the approach can be replicated in the design process of similar kinds of spatially distributed Internet-of-Things systems.

cs.DC↗

arXiv2019

Perpetual Assurances for Self-Adaptive Systems

Providing assurances for self-adaptive systems is challenging. A primary underlying problem is uncertainty that may stem from a variety of different sources, ranging from incomplete knowledge to sensor noise and uncertain behavior of humans in the loop. Providing assurances that the self-adaptive system complies with its requirements calls for an enduring process spanning the whole lifetime of the system. In this process, humans and the system jointly derive and integrate new evidence and arguments, which we coined perpetual assurances for self-adaptive systems. In this paper, we provide a background framework and the foundation for perpetual assurances for self-adaptive systems. We elaborate on the concrete challenges of offering perpetual assurances, requirements for solutions, realization techniques and mechanisms to make solutions suitable. We also present benchmark criteria to compare solutions. We then present a concrete exemplar that researchers can use to assess and compare approaches for perpetual assurances for self-adaptation.

cs.SE↗

arXiv2019

Specification Patterns for Robotic Missions

Mobile and general-purpose robots increasingly support our everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing their complex behaviors known as missions. Recognizing the need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation, or guiding the implementation. For instance, the logical language LTL is commonly used by experts to specify missions, as an input for planners, which synthesize the behavior a robot should have. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems, each of which detailing the usage intent, known uses, relationships to other patterns, and---most importantly---a template mission specification in temporal logic. Our tooling produces specifications expressed in the LTL and CTL temporal logics to be used by planners, simulators, or model checkers. The patterns originate from 245 realistic textual mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios we defined with two well-known industrial partners developing human-size robots. We validated our patterns' correctness with simulators and two real robots.

cs.SE↗

arXiv2016

An EMOF-Compliant Abstract Syntax for Bigraphs

Bigraphs are an emerging modeling formalism for structures in ubiquitous computing. Besides an algebraic notation, which can be adopted to provide an algebraic syntax for bigraphs, the bigraphical theory introduces a visual concrete syntax which is intuitive and unambiguous at the same time; the standard visual notation can be customized and thus tailored to domain-specific requirements. However, in contrast to modeling standards based on the Meta-Object Facility (MOF) and domain-specific languages typically used in model-driven engineering (MDE), the bigraphical theory lacks a precise definition of an abstract syntax for bigraphical modeling languages. As a consequence, available modeling and analysis tools use proprietary formats for representing bigraphs internally and persistently, which hampers the exchange of models across tool boundaries. Moreover, tools can be hardly integrated with standard MDE technologies in order to build sophisticated tool chains and modeling environments, as required for systematic engineering of large systems or fostering experimental work to evaluate the bigraphical theory in real-world applications. To overcome this situation, we propose an abstract syntax for bigraphs which is compliant to the Essential MOF (EMOF) standard defined by the Object Management Group (OMG). We use typed graphs as a formal underpinning of EMOF-based models and present a canonical mapping which maps bigraphs to typed graphs in a natural way. We also discuss application-specific variation points in the graph-based representation of bigraphs. Following standard techniques from software product line engineering, we present a framework to customize the graph-based representation to support a variety of application scenarios.

cs.SE↗

arXiv2016

Modeling, refining and analyzing Incomplete Büchi Automata

Software development is an iterative process which includes a set of development steps that transform the initial high level specification of the system into its final, fully specified, implementation. This report discusses the theoretical foundations that allow Incomplete Büchi Automata (IBAs) to be used in the iterative development of a sequential system.

cs.FL↗

arXiv2015

Efficient Large-scale Trace Checking Using MapReduce

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches. In this paper we address this memory scalability issue by proposing a new semantics for MTL, called lazy semantics. This semantics can evaluate temporal formulae and boolean combinations of temporal-only formulae at any arbitrary time instant. We prove that lazy semantics is more expressive than standard point-based semantics and that it can be used as a basis for a correct parametric decomposition of any MTL formula into an equivalent one with smaller, bounded time intervals. We use lazy semantics to extend our previous distributed trace checking algorithm for MTL. We evaluate the proposed algorithm in terms of memory scalability and time/memory tradeoffs.

cs.SE↗

arXiv2015

Enhancing Reuse of Constraint Solutions to Improve Symbolic Execution

Constraint solution reuse is an effective approach to save the time of constraint solving in symbolic execution. Most of the existing reuse approaches are based on syntactic or semantic equivalence of constraints; e.g. the Green framework is able to reuse constraints which have different representations but are semantically equivalent, through canonizing constraints into syntactically equivalent normal forms. However, syntactic/semantic equivalence is not a necessary condition for reuse--some constraints are not syntactically or semantically equivalent, but their solutions still have potential for reuse. Existing approaches are unable to recognize and reuse such constraints. In this paper, we present GreenTrie, an extension to the Green framework, which supports constraint reuse based on the logical implication relations among constraints. GreenTrie provides a component, called L-Trie, which stores constraints and solutions into tries, indexed by an implication partial order graph of constraints. L-Trie is able to carry out logical reduction and logical subset and superset querying for given constraints, to check for reuse of previously solved constraints. We report the results of an experimental assessment of GreenTrie against the original Green framework, which shows that our extension achieves better reuse of constraint solving result and saves significant symbolic execution time.

cs.SE↗

arXiv2014

Offline Trace Checking of Quantitative Properties of Service-Based Applications

Service-based applications are often developed as compositions of partner services. A service integrator needs precise methods to specify the quality attributes expected by each partner service, as well as effective techniques to verify these attributes. In previous work, we identified the most common specification patterns related to provisioning service-based applications and developed an expressive specification language (SOLOIST) that supports them. SOLOIST is an extension of metric temporal logic with aggregate temporal modalities that can be used to write quantitative temporal properties. In this paper we address the problem of performing offline checking of service execution traces against quantitative requirements specifications written in SOLOIST. We present a translation of SOLOIST into CLTLB(D), a variant of linear temporal logic, and reduce the trace checking of SOLOIST to bounded satisfiability checking of CLTLB(D), which is supported by ZOT, an SMT-based verification toolkit. We detail the results of applying the proposed offline trace checking procedure to different types of traces, and compare its performance with previous work.

cs.SE↗

arXiv2014

Trace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce

Modern complex software systems produce a large amount of execution data, often stored in logs. These logs can be analyzed using trace checking techniques to check whether the system complies with its requirements specifications. Often these specifications express quantitative properties of the system, which include timing constraints as well as higher-level constraints on the occurrences of significant events, expressed using aggregate operators. In this paper we present an algorithm that exploits the MapReduce programming model to check specifications expressed in a metric temporal logic with aggregating modalities, over large execution traces. The algorithm exploits the structure of the formula to parallelize the evaluation, with a significant gain in time. We report on the assessment of the implementation - based on the Hadoop framework - of the proposed algorithm and comment on its scalability.

cs.SE↗

arXiv2013

Verification for Reliable Product Lines

Many product lines are critical, and therefore reliability is a vital part of their requirements. Reliability is a probabilistic property. We therefore propose a model for feature-aware discrete-time Markov chains as a basis for verifying probabilistic properties of product lines, including reliability. We compare three verification techniques: The enumerative technique uses PRISM, a state-of-the-art symbolic probabilistic model checker, on each product. The parametric technique exploits our recent advances in parametric model checking. Finally, we propose a new bounded technique that performs a single bounded verification for the whole product line, and thus takes advantage of the common behaviours of the product line. Experimental results confirm the advantages of the last two techniques.

cs.SE↗

arXiv2013

A Syntactic-Semantic Approach to Incremental Verification

Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices for evolving systems. Since changes in these systems are often local to restricted parts, an incremental verification approach could be beneficial. This paper introduces SiDECAR, a general framework for the definition of verification procedures, which are made incremental by the framework itself. Verification procedures are driven by the syntactic structure (defined by a grammar) of the system and encoded as semantic attributes associated with the grammar. Incrementality is achieved by coupling the evaluation of semantic attributes with an incremental parsing technique. We show the application of SiDECAR to the definition of two verification procedures: probabilistic verification of reliability requirements and verification of safety properties.

cs.SE↗

arXiv2012

Context-Oriented Programming: A Programming Paradigm for Autonomic Systems

Dynamic software adaptability is one of the central features leveraged by autonomic computing. However, developing software that changes its behavior at run time adapting to the operational conditions is a challenging task. Several approaches have been proposed in the literature to attack this problem at different and complementary abstraction levels: software architecture, middleware, and programming level. We focus on the support that ad-hoc programming language constructs may provide to support dynamically adaptive behaviors. We introduce context-oriented programming languages and we present a framework that positions the supported paradigm in the MAPE-K autonomic loop. We discuss the advantages of using context-oriented programming languages instead of other mainstream approaches based on dynamic aspect oriented programming languages and present a case study that shows how the proposed programming style naturally fits dynamic adaptation requirements. Finally, we discuss some known problems and outline a number of open research challenges.

cs.PL↗

arXiv2011

JavaCtx: Seamless Toolchain Integration for Context-Oriented Programming

Context-oriented programming is an emerging paradigm addressing at the language level the issue of dynamic software adaptation and modularization of context-specific concerns. In this paper we propose JavaCtx, a tool which employs coding conventions to generate the context-aware semantics for Java programs and subsequently weave it into the application. The contribution of JavaCtx is twofold: the design of a set of coding conventions which allow to write context-oriented software in plain Java and the concept of context-oriented semantics injection, which allows to introduce the context-aware semantics without a source-to-source compilations process which disrupts the structure of the code. Both these points allow to seamless integrate JavaCtx in the existing industrial-strength appliances and by far ease the development of context-oriented software.

cs.PL↗