| 1. |
- Andersson, Jesper, et al.
(författare)
-
Software Engineering Processes for Self-adaptive Systems
- 2013
-
Ingår i: Software Engineering for Self-Adaptive Systems International Seminar Dagstuhl Castle, Germany, October 24-29, 2010 Revised Selected and Invited Papers. - Berlin, Heidelberg : Springer. - 9783642358128 - 9783642358135 ; , s. 51-75
-
Bokkapitel (refereegranskat)abstract
- In this paper, we discuss how for self-adaptive systems someactivities that traditionally occur at development-time are moved to runtime. Responsibilities for these activities shift from software engineers tothe system itself, causing the traditional boundary between development time and run-time to blur. As a consequence, we argue how the traditional software engineering process needs to be reconceptualized to distinguishvboth development-time and run-time activities, and to support designers in taking decisions on how to properly engineer such systems.Furthermore, we identify a number of challenges related to this required reconceptualization, and we propose initial ideas based on process modeling.We use the Software and Systems Process Engineering Meta-Model(SPEM) to specify which activities are meant to be performed o-line andon-line, and also the dependencies between them. The proposed models should capture information about the costs and benets of shifting activitiesto run-time, since such models should support software engineers in their decisions when they are engineering self-adaptive systems.
|
|
| 2. |
- Autili, Marco, et al.
(författare)
-
Automated Synthesis of Application-layer Connectors from Automata-based Specifications
- 2015
-
Ingår i: Language and Automata Theory and Applications. - Cham : Springer. ; , s. 3-24
-
Konferensbidrag (refereegranskat)abstract
- The heterogeneity characterizing the systems populating the Ubiquitous Computing environment prevents their seamless interoperability. Heterogeneous protocols may be willing to cooperate in order to reach some common goal even though they meet dynamically and do not have a priori knowledge of each other. Despite numerous efforts have been done in the literature, the automated and run-time interoperability is still an open challenge for such environment. We consider interoperability as the ability for two Networked Systems (NSs) to communicate and correctly coordinate to achieve their goal(s). In this paper, we report the main outcomes of our past and recent research on automatically achieving protocol interoperability via connector synthesis. We consider application-layer connectors by referring to two conceptually distinct notions of connector: {\em coordinator} and {\em mediator}. The former is used when the NSs to be connected are already able to communicate but they need to be specifically coordinated in order to reach their goal(s). The latter goes a step forward representing a solution for both achieving correct coordination and enabling communication between highly heterogeneous NSs. In the past, most of the works in the literature described efforts to the automatic synthesis of coordinators while, in recent years the focus moved also to the automatic synthesis of mediators. By considering our past experience on the automatic synthesis of coordinators and mediators as a baseline, we conclude by overviewing a formal method for the automated synthesis of mediators that allows to relax some assumptions state-of-the-art approaches rely on, and characterize the necessary and sufficient interoperability conditions that ensure the mediator existence and correctness.
|
|
| 3. |
- Autili, Marco, et al.
(författare)
-
Automated synthesis of application-layer connectors from automata-based specifications
- 2019
-
Ingår i: Journal of computer and system sciences (Print). - : Elsevier. - 0022-0000 .- 1090-2724. ; 104, s. 17-40
-
Tidskriftsartikel (refereegranskat)abstract
- Ubiquitous and Pervasive Computing, and the Internet of Things, promote dynamic interaction among heterogeneous systems. To achieve this vision, interoperability among heterogeneous systems represents a key enabler, and mediators are often built to solve protocol mismatches. Many approaches propose the synthesis of mediators. Unfortunately, a rigorous characterization of the concept of interoperability is still lacking, hence making hard to assess their applicability and soundness. In this paper, we provide a framework for the synthesis of mediators that allows us to: (i) characterize the conditions for the mediator existence and correctness; and (ii) establish the applicability boundaries of the synthesis method.
|
|
| 4. |
- Calinescu, Radu, et al.
(författare)
-
Synthesis and Verification of Self-aware Computing Systems
- 2017
-
Ingår i: Self-aware Computing Systems. - Cham : Springer. - 9783319474724 ; , s. 337-373
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Self-aware computing systems are envisaged to exploit the knowledge of their own software architecture, hardware infrastructure and environment in order to follow high-level goals through proactively adapting as their environment evolves. This chapter describes two classes of key enabling techniques for self-adaptive systems: automated synthesis and formal verification. The ability to dynamically synthesize component connectors and compositions underpins the proactive adaptation of the architecture of self-aware systems. Deciding when adaptation is needed and selecting valid new architectures or parameters for self-aware systems often requires formal verification. We present the state of the art in the use of the two techniques for the development of self-aware computing systems and summarize the main research challenges associated with their adoption in practice.
|
|
| 5. |
- Caporuscio, Mauro, 1975-, et al.
(författare)
-
Compositional Verification of Middleware-Based Software Architecture Descriptions
- 2004
-
Ingår i: Proceedings of the 26th International Conference on Software Engineering (ICSE '04). - : IEEE Press. ; , s. 221-230
-
Konferensbidrag (refereegranskat)abstract
- In this paper we present a compositional reasoning to verify middleware-based software architecturedescriptions. We consider a nowadays typical software system development, namely the development of a software application A on a middleware M. Our goal is to efficiently integrate verification techniques, like model checking, in the software life cycle in order to improve the overall software quality. The approach exploits the structure imposed on the system by the software architecture in order to develop an assume-guarantee methodology to reduce properties verification from global to local. We apply the methodology on a non-trivial case study namely the development of a Gnutella system on top of the SIENA event-notification middleware.
|
|
| 6. |
- Caporuscio, Mauro, 1975-, et al.
(författare)
-
Engineering MDA into Compositional Reasoning for Analyzing Middleware-Based Applications
- 2005
-
Ingår i: Software Architecture. - Berlin, Heidelberg : Springer. - 9783540262756 ; , s. 130-145
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Behavioral analysis of middleware-based applications typically requires the analysis of the middleware and the application, in a monolithic way. In terms of model-checking, this is a complex task and may result in the well known “state-explosion” problem. These considerations led us to investigate a compositional verification approach which decomposes the system in accordance with its Software Architecture. The architectural decomposability theorem we defined in previous work decomposes the system into three logical layer: (i) application components, (ii) proxies and, (iii)middleware. This logical separation allows for reducing the global system validation to the verification of local behaviors.In this paper, we engineer the architectural decomposability theorem to the analysis of middleware-based applications by automatically generating the proxies needed by the components in order to properly interact with each other via the middleware. In particular, following the Model Driven Architecture approach and by making use of the Abstract State Machine formalism, we describe a set of transformation rules that allow for deriving correct proxies for using CORBA. By means of the proposed transformations, the correctness of the proxy behavioral models is guaranteed without the need to validate them with respect to the assumptions posed by the theorem.
|
|
| 7. |
- Caporuscio, Mauro, 1975-, et al.
(författare)
-
Formal Analysis of Architectural Patterns
- 2004
-
Ingår i: Software Architecture. - Berlin, Heidelberg : Springer. - 9783540220008 ; , s. 10-24
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Architectural patterns characterize and specify structural and behavioral properties of (sub)systems, thus allowing the provision of solutions for classes of problems.In this paper we show the use of architectural patterns as an abstraction to carry on, and reuse, formal reasoning on systems whose configuration can dynamically change.This kind of systems is hard to model and to reason about due to the fact that we cannot simply build a model with fixed topology (i.e. fixed number of components and connectors) and validate properties of interest on it.The work presented in this paper proposes an approach that given an architectural pattern which expresses a class of systems configurations and a set of properties of interest (i) selects, if any, aminimal configuration for which the specified properties make sense, (ii) an abstraction of the chosen architectural model erformed, in order to reduce the complexity of the verification phase. In this stage, abstractions are driven by the properties of interest. The output of this abstraction step can be model-checked, tested and analyzed by using a standard model-checking framework. (iii) The verification results obtained in the previous step are lifted to generic configurations by performing manual reasoning driven by the constraints posed by the architectural pattern.The approach will be applied by using an event-based architectural pattern to a publish/subscribe system, the Siena middleware, in order to validate its features and its mobility extension.
|
|
| 8. |
- Caporuscio, Mauro, 1975-, et al.
(författare)
-
Model-based system reconfiguration for dynamic performance management
- 2007
-
Ingår i: Journal of Systems and Software. - : Elsevier. - 0164-1212 .- 1873-1228. ; 80:4, s. 455-473
-
Tidskriftsartikel (refereegranskat)abstract
- Recently, growing attention focused on run-time management of Quality of Service (QoS) of complex software systems. In this context, system reconfiguration is considered a useful technique to manage QoS. Several reconfiguration approaches to performance management exist that help systems to maintain performance requirements at run time. However, many of them use prefixed strategies that are in general coded in the application or in the reconfiguration framework.In this work we propose a framework to manage performance of software systems at run time based on monitoring and model-based performance evaluation. The approach makes use of software architectures as abstractions of the managed system to avoid unnecessary details that can heavily affect the model evaluation in terms of complexity and resolution time.
|
|
| 9. |
- Caporuscio, Mauro, 1975-, et al.
(författare)
-
Run-time Performance Management of the Siena Publish/Subscribe Middleware
- 2005
-
Ingår i: Proceedings of the 5th International Workshop on Software and Performance (WOSP '05). - New York, NY, USA : ACM Press. - 1595930876 ; , s. 65-74
-
Konferensbidrag (refereegranskat)abstract
- Recently, growing attention is focused on run-time management of Quality of Service (QoS) of complex software systems. In this context, self-adaptation of applications, based on runtime monitoring and dynamic reconfiguration, is considered a useful technique to manage/negotiate QoS. Several defined approaches to dynamic performance management propose the use of on-line model-based evaluation of the managed application in order to choose the new application configuration for improving the QoS. In a previous work we defined a methodology to manage performance of soft-ware system at run-time based on model-based performance evaluation. To avoid unnecessary details the performance model represents the managed application at the Software Architecture level. In this work we apply and implement this approach to dynamic manage the performance of the SIENA publish/subscribe event notification service.
|
|
| 10. |
- Caporuscio, Mauro, 1975-, et al.
(författare)
-
Uncertain Event-based Model for Egocentric Context Sensing
- 2005
-
Ingår i: Proceedings of the 5th International Workshop on Software Engineering and Middleware. - New York, NY, USA : ACM. ; , s. 25-32
-
Konferensbidrag (refereegranskat)abstract
- Calm Technology characterizes those technologies that move forth and back between the center and periphery of our attention. That is, while center denotes what one is currently focused on, periphery denotes what one is attuned to without focusing on it explicitly. Context-aware computing exploits such a concept by allowing applications to adapt their behavior (i.e. the center) in response to the context sensed within the environment (i.e. the periphery). An application in this setting should have minimal assumptions in order to operate while being able to dynamically adapt to and learn what the surrounding context offers.In this paper we discuss ongoing work in designing an event-based model that allows applications to egocentrically perceive the periphery and evaluate its relevance and uncertainty with respect to the center of the application attention. In particular we discuss our ongoing work in designing and developing ECHOES, an uncertain event-model for Egocentric computing. Characteristics of ECHOES are (a) departing from usual conjunctive pattern-matching algorithms implemented in event-notification models and, (b) achieving event correlation through the use of complex filters defined by means of Fuzzy Logic formulas. The paper introduces the specification of ECHOES as well as the design of an early prototype developed as a modified implementation of the SIENA Publish/Subscribe Middleware.
|
|
| 11. |
- Caporuscio, Mauro, 1975-, et al.
(författare)
-
Yet Another Framework for Supporting Mobile and Collaborative Work
- 2003
-
Ingår i: Proceedings. Twelfth IEEE International Workshops on Enabling Technologies, 2003. WET ICE 2003.. - : IEEE Press. - 0769519636 ; , s. 81-86
-
Konferensbidrag (refereegranskat)abstract
- This paper presents the design of YACO (Yet Another framework for Collaborative work), a framework for supporting mobile collaborative work. Mobile collaborative work has been increasing in popularity in business domain. Coworkers cooperate and share expertise across sites and domains, employees may move from a location to another carrying devices (such as PDAs and laptops) in which they store documents. The YACO framework that we have designed aims at exploiting the capabilities provided by an event-based system with support for mobile application in order to offer services to users that collaborates each other in a corporate domain.
|
|
| 12. |
|
|
| 13. |
- de Lemos, Rogerio, et al.
(författare)
-
Software Engineering for Self-Adaptive Systems : A Second Research Roadmap
- 2013
-
Ingår i: Software Engineering for Self-Adaptive Systems II. - Berlin, Heidelberg : Springer. - 9783642358128 ; , s. 1-32
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- The goal of this roadmap paper is to summarize the state-of-the-art and identify research challenges when developing, deploying and managing self-adaptive software systems. Instead of dealing with a wide range of topics associated with the field, we focus on four essential topics of self-adaptation: design space for self-adaptive solutions, software engineering processes for self-adaptive systems, from centralized to decentralized control, and practical run-time verification & validation for self-adaptive systems. For each topic, we present an overview, suggest future directions, and focus on selected challenges. This paper complements and extends a previous roadmap on software engineering for self-adaptive systems published in 2009 covering a different set of topics, and reflecting in part on the previous paper. This roadmap is one of the many results of the Dagstuhl Seminar 10431 on Software Engineering for Self-Adaptive Systems, which took place in October 2010.
|
|
| 14. |
|
|
| 15. |
- Johnsen, Andreas
(författare)
-
Quality Assurance for Dependable Embedded Systems
- 2018
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Architectural engineering of embedded computer systems comprehensively affects both the development processes and the abilities of the systems. Rigorous and holistic verification of architectural engineering is consequently essential in the development of safety-critical and mission-critical embedded systems, such as computer systems within aviation, automotive, and railway transportation, where even minor architectural defects may cause substantial cost and devastating harm. The increasing complexity of embedded systems renders this challenge unmanageable without the support of automated methods of verification, to reduce the cost of labor and the risk of human error.The contribution of this thesis is an Architecture Quality Assurance Framework (AQAF) and a corresponding tool support, the Architecture Quality Assurance Tool (AQAT). AQAF provides a rigorous, holistic, and automated solution to the verification of critical embedded systems architectural engineering, from requirements analysis and design to implementation and maintenance. A rigorous and automated verification across the development process is achieved through the adaption and integration of formal methods to architectural engineering. The framework includes an architectural model checking technique for the detection of design faults, an architectural model-based test suite generation technique for the detection of implementation faults, and an architectural selective regression verification technique for an efficient detection of faults introduced by maintenance modifications.An integrated solution provides traceability and coherency between the verification processes and the different artifacts under analysis, which is essential for obtaining reliable results, for meeting certification provisions, and for performing impact analyses of maintenance modifications. The Architecture Quality Assurance Tool (AQAT) implements the theory of AQAF and enables an effortless adoption into industrial practices. Empirical results from an industrial study present a high fault detection rate at both the design level and the implementation level as well as an efficient selective regression verification process. Furthermore, the results of a scalability evaluation show that the solution is scalable to complex many-core embedded systems with multithreading.
|
|
| 16. |
- Kunnappilly, Ashalatha
(författare)
-
Modeling and Formal Analysis of e-Health Systems
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- With the healthcare practice being increasingly dependent on digital processes and electronic communication, there is a need to support a variety of e-Health applications of different requirements, with respect to connectivity, low latency, and high reliability. The focus of this thesis is on providing formal assurance to systems supporting e-Health applications. Among such systems, this thesis considers: a) Ambient Assisted Living (AAL) Systems, aimed to assist the elderly in their independent and safe living within their homes, and b) healthcare assistance systems that include home, hospital, or emergency e-Health applications, where simultaneous access and communication is critical.In order to provide formal assurance, one needs to capture both the structure and behavior of the targeted e-Health systems within models that can be formalized and analyzed by formal methods. Due to only few existing initiatives in the AAL domain that integrate common AAL functionalities such as pulse monitoring, fall detection, as well as fire detection, and remote communication with care-givers, within a generic framework, in this thesis, we propose, as a first contribution, two different categories of AAL architecture frameworks onto which different functionalities, chosen based on user preferences, can be integrated. The first solution follows a centralized approach, using an intelligent Decision Support System, and the second employs a distributed architectural approach, involving multiple intelligent agents. Although centralized solutions are easy to develop, scalability, flexibility, multiple user accesses and potential self-healing are easier to achieve with the distributed, agent-based architecture. To formally assure these solutions against functional, timing and reliability requirements, as a second contribution, we model the architectures in one of the architecture description languages, namely Architecture Analysis and Design Language, to which we assign semantics in terms of various flavors of transition systems. Consequently, we employ corresponding model checking techniques, such as exhaustive model checking in UPPAAL, statistical model checking in UPPAAL SMC, and probabilistic Model Checking in PRISM, to provide the necessary design-time assurance. Our AAL formal frameworks abstract away the communication media and assume communication protocols with fixed delays only. Moreover, their scope is limited to home-based assistance with with no simultaneous/parallel user access. Hence, we model next the communication media and expand our scope to target generic e-Health systems supporting home, hospital, and emergency use cases. For such systems, networking capabilities with real-time and reliable communication schemes are essential for service-user connectivity, and resource sharing.One communication scheme employed in such e-Health applications is the fifth generation of cellular wireless technology, namely, 5G, which offers the possibility of creating network slices that provide independent logical networks, to serve a variety of applications characterized by certain quality-of-service requirements. The network slicing is enabled by the underlying 5G service orchestration capabilities that deal with virtual network function placement, implicit resource assignment, and traffic routing.In this work, we study in detail the service orchestration problem in 5G. As the third contribution, we propose a UML-based framework consisting of: (a) a UML5G Service Orchestration Profile (UML5G-SO) that facilitates modeling service orchestration and network slicing for such 5G-based systems, and (b) associated analysis techniques that back the profile, namely logic-based analysis using the USE tool, and exhaustive model checking via UPPAAL. As a final contribution, we propose a tool that integrates UML5G-SO models with UPPAAL, and apply our framework on real use cases of e-Health systems, to provide some experimental evaluation by which we gather useful insights with respect to the framework's practical strengths and weaknesses.Our work in this thesis paves the way towards the development of healthcare assistance systems with assured quality of service.
|
|
| 17. |
- Nostro, Nicola, et al.
(författare)
-
Achieving functional and non functional interoperability through synthesized connectors
- 2016
-
Ingår i: Journal of Systems and Software. - : Elsevier. - 0164-1212 .- 1873-1228. ; 111, s. 185-199
-
Tidskriftsartikel (refereegranskat)abstract
- Our everyday life is pervaded by the use of a number of heterogeneous systems that are continuously and dynamically available in the networked environment to interoperate to achieve some goal. Goals may include both functional and non functional aspects and the evolving nature of such environment requires automated solutions as means to reach the needed level of flexibility. Achieving interoperability in such environment is a challenging problem. Even though some of such systems may in principle interact since they have compatible functionalities and similar interaction protocols, mismatches in their protocols and non functional issues arising from the environment may undermine their seamless interoperability. In this paper, we propose an approach for the automated synthesis of application layer connectors between heterogeneous Networked Systems (NSs) addressing both functional and some non functional interoperability. Our contributions are: (i) an automated connectors synthesis approach for NSs interoperability taking into account functional, performance and dependability aspects spanning pre-deployment time and run-time; (ii) a connector adaptation process, related to the performance and dependability aspects; and (iii) a stochastic model-based implementation of the performance and dependability analysis. In addition, we implemented, analysed, and critically discussed a case study.
|
|
| 18. |
- Scoccia, Gian Luca, et al.
(författare)
-
Hey, my data are mine! Active data to empower the user
- 2020
-
Ingår i: Proceedings - International Conference on Software Engineering. - New York, NY, USA : ACM. - 0270-5257. ; , s. 5-8
-
Konferensbidrag (refereegranskat)abstract
- Privacy is increasingly getting importance in modern systems. As a matter of fact, personal data are out of the control of the original owner and remain in the hands of the software-systems producers. In this new ideas paper, we drastically change the nature of data from passive to active as a way to empower the user and preserve both the original ownership of the data and the privacy policies specified by the data owner. We demonstrate the idea of active data in the mobile domain.
|
|
| 19. |
- Weyns, Danny, et al.
(författare)
-
Perpetual assurances for self-adaptive systems
- 2017
-
Ingår i: Software Engineeringfor Self-Adaptive Systems III, Assurances. - Cham : Springer. - 9783319741826 - 9783319741833 ; , s. 31-63
-
Bokkapitel (refereegranskat)abstract
- 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. © Springer International Publishing AG 2017.
|
|
