BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Carlo Ghezzi

Carlo Ghezzi appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Software EngineeringProgramming LanguagesDistributed, Parallel, and Cluster ComputingFormal Languages and Automata TheoryLogic in Computer ScienceMultiagent SystemsNetworking and Internet Architecture

Catalog footprint

What is connected

12works
7topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

12 published item(s)

preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

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.

0 citations0 reviewsNo code linkedOpen access