-
A Systematic Literature Review on a Decade of Industrial TLA+ Practice
Authors:
Roman Bögli,
Leandro Lerena,
Christos Tsigkanos,
Timo Kehrer
Abstract:
TLA+ is a formal specification language used for designing, modeling, documenting, and verifying systems through model checking. Despite significant interest from the research community, knowledge about usage of the TLA+ ecosystem in practice remains scarce. Industry reports suggest that software engineers could benefit from insights, innovations, and solutions to the practical challenges of TLA+.…
▽ More
TLA+ is a formal specification language used for designing, modeling, documenting, and verifying systems through model checking. Despite significant interest from the research community, knowledge about usage of the TLA+ ecosystem in practice remains scarce. Industry reports suggest that software engineers could benefit from insights, innovations, and solutions to the practical challenges of TLA+. This paper explores this development by conducting a systematic literature review of TLA+'s industrial usage over the past decade. We analyze the trend in industrial application, characterize its use, examine whether its promised benefits resonate with practitioners, and identify challenges that may hinder further adoption.
△ Less
Submitted 20 November, 2024;
originally announced November 2024.
-
Early Validation of Cyber-Physical Space Systems via Multi-Concerns Integration
Authors:
Nianyu Li,
Christos Tsigkanos,
Zhi Jin,
Zhenjiang Hu,
Carlo Ghezzi
Abstract:
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…
▽ More
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.
△ Less
Submitted 13 July, 2020;
originally announced July 2020.
-
Cloud Deployment Tradeoffs for the Analysis of Spatially-Distributed Systems of Internet-of-Things
Authors:
Christos Tsigkanos,
Martin Garriga,
Luciano Baresi,
Carlo Ghezzi
Abstract:
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 i…
▽ More
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.
△ Less
Submitted 23 April, 2020;
originally announced April 2020.
-
Sabrina: Modeling and Visualization of Economy Data with Incremental Domain Knowledge
Authors:
Alessio Arleo,
Christos Tsigkanos,
Chao Jia,
Roger A. Leite,
Ilir Murturi,
Manfred Klaffenboeck,
Schahram Dustdar,
Michael Wimmer,
Silvia Miksch,
Johannes Sorger
Abstract:
Investment planning requires knowledge of the financial landscape on a large scale, both in terms of geo-spatial and industry sector distribution. There is plenty of data available, but it is scattered across heterogeneous sources (newspapers, open data, etc.), which makes it difficult for financial analysts to understand the big picture. In this paper, we present Sabrina, a financial data analysi…
▽ More
Investment planning requires knowledge of the financial landscape on a large scale, both in terms of geo-spatial and industry sector distribution. There is plenty of data available, but it is scattered across heterogeneous sources (newspapers, open data, etc.), which makes it difficult for financial analysts to understand the big picture. In this paper, we present Sabrina, a financial data analysis and visualization approach that incorporates a pipeline for the generation of firm-to-firm financial transaction networks. The pipeline is capable of fusing the ground truth on individual firms in a region with (incremental) domain knowledge on general macroscopic aspects of the economy. Sabrina unites these heterogeneous data sources within a uniform visual interface that enables the visual analysis process. In a user study with three domain experts, we illustrate the usefulness of Sabrina, which eases their analysis process.
△ Less
Submitted 8 January, 2020; v1 submitted 5 August, 2019;
originally announced August 2019.
-
Specification Patterns for Robotic Missions
Authors:
Claudio Menghi,
Christos Tsigkanos,
Patrizio Pelliccione,
Carlo Ghezzi,
Thorsten Berger
Abstract:
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 spe…
▽ More
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.
△ Less
Submitted 7 January, 2019;
originally announced January 2019.
-
An EMOF-Compliant Abstract Syntax for Bigraphs
Authors:
Timo Kehrer,
Christos Tsigkanos,
Carlo Ghezzi
Abstract:
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,…
▽ More
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.
△ Less
Submitted 5 December, 2016;
originally announced December 2016.
