mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Alternative names
Publications (10 of 104) Show all publications
Kunnappilly, A., Marinescu, R. & Seceleanu, C. (2019). A Model-Checking-Based Framework For Analyzing Ambient Assisted Living Solutions. Sweden
Open this publication in new window or tab >>A Model-Checking-Based Framework For Analyzing Ambient Assisted Living Solutions
2019 (English)Report (Refereed)
Place, publisher, year, edition, pages
Sweden: , 2019
National Category
Embedded Systems
Identifiers
urn:nbn:se:mdh:diva-42920 (URN)
Note

Since modern ambient assisted living solutions integrate a multitude of assisted-living functionalities within a common design framework, some are safety-critical, it is desirable that these systems are analyzed already at their design stage to detect possible errors. To achieve this, one needs suitable architectures that support the seamless design of the integrated assisted-living functions, as well as capabilities for the formal modeling and analysis of the architecture. In this paper, we attempt to address this need, by proposing a generic integrated ambient assisted living system architecture, consisting of sensors, data-collector, local and cloud processing schemes, and an intelligent decision support system, which can be easily extended to suite specific architecture categories. Our solution is customizable, therefore, we show three instantiations of the generic model, as simple, intermediate and complex configuration, respectively, and show how to analyze the first and third categories by model checking. Our approach starts by specifying the architecture, using an architecture description language, in our case, the Architecture Analysis and Design Language that can also account for the probabilistic behavior of such systems. To enable formal analysis, we describe the semantics of the simple and complex categories as stochastic timed automata. The former we model check exhaustively with UPPAAL, whereas for the latter we employ statistical model checking using UPPAAL SMC, the statistical extension of UPPAAL, for scalability reasons.

Available from: 2019-03-14 Created: 2019-03-14 Last updated: 2019-06-11Bibliographically approved
Kunnappiilly, A., Cai, S., Marinescu, R. & Seceleanu, C. (2019). Architecture modelling and formal analysis of intelligent multi-agent systems. In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering: . Paper presented at 14th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2019, 4 May 2019 through 5 May 2019 (pp. 114-126). SciTePress
Open this publication in new window or tab >>Architecture modelling and formal analysis of intelligent multi-agent systems
2019 (English)In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering, SciTePress , 2019, p. 114-126Conference paper, Published paper (Refereed)
Abstract [en]

Modern cyber-physical systems usually assume a certain degree of autonomy. Such systems, like Ambient Assisted Living systems aimed at assisting elderly people in their daily life, often need to perform safety-critical functions, for instance, fall detection, health deviation monitoring, communication to caregivers, etc. In many cases, the system users have distributed locations, as well as different needs that need to be serviced intelligently and simultaneously. These features call for intelligent, adaptive, scalable and fault-tolerant system design solutions, which are well embodied by multi-agent architectures. Analyzing such complex architectures at design phase, to verify if an abstraction of the system satisfies all the critical requirements is beneficial. In this paper, we start from an agent-based architecture for ambient assisted living systems, inspired from the literature, which we model in the popular Architecture Analysis and Design Language. Since the latter lacks the ability to specify autonomous agent behaviours, which are often intelligent, non deterministic or probabilistic, we extend the architectural language with a sub-language called Agent Annex, which we formally encode as a Stochastic Transition System. This contribution allows us to specify behaviours of agents involved in agent-based architectures of cyber-physical systems, which we show how to exhaustively verify with the state-of-art model checker PRISM. As a final step, we apply our framework on a distributed ambient assisted living system, whose critical requirements we verify with PRISM.

Place, publisher, year, edition, pages
SciTePress, 2019
Keywords
Ambient Assisted Living, Architecture Analsysis And Design Language, Cyber-physical Systems, Model Checking, Multi-Agent Systems, PRISM, Assisted living, Autonomous agents, Biological systems, Computer architecture, Cyber Physical System, Embedded systems, Intelligent agents, Prisms, Safety engineering, Stochastic systems, Systems analysis, Agent based architectures, Architectural languages, Design languages, Intelligent multi agent systems, Multiagent architecture, Safety-critical functions, Stochastic transition systems, Multi agent systems
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-44882 (URN)2-s2.0-85067426971 (Scopus ID)9789897583759 (ISBN)
Conference
14th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2019, 4 May 2019 through 5 May 2019
Note

Conference code: 148432; Export Date: 11 July 2019; Conference Paper

Available from: 2019-07-11 Created: 2019-07-11 Last updated: 2019-07-11Bibliographically approved
Filipovikj, P., Rodriguez-Navas, G. & Seceleanu, C. (2019). Bounded Invariance Checking of Simulink Models. In: Proceedings of the ACM Symposium on Applied Computing: . Paper presented at SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019 (pp. 2168-2177). , Part F147772
Open this publication in new window or tab >>Bounded Invariance Checking of Simulink Models
2019 (English)In: Proceedings of the ACM Symposium on Applied Computing, 2019, Vol. Part F147772, p. 2168-2177Conference paper, Published paper (Refereed)
Abstract [en]

Currently, Simulink models can be verified rigorously against design errors or statistical properties. In this paper, we show how Simulink models can be formally analyzed against invariance properties using bounded model checking reduced to satisfiability modulo theories solving. In its basic form, the technique provides means for verification of an underlying model over bounded traces rigorously, however, in general the procedure is incomplete. We identify common Simulink block types and compositions by analyzing selected industrial models, and we show that for some of them the set of non-repeating states (reachability diameter) can be visited with a finite set of paths of finite length, yielding the verification complete. We complement our approach with a tool, called SyMC that automates the following: i) calculation of the reachability diameter size for some of the designs, ii) generation of finite (bounded) paths of the underlying Simulink model and their encoding into SMT-LIB format and iii) checking invariance properties using the Z3 SMT solver. To show the applicability of our approach, we apply it on a prototype implementation of an industrial Simulink model, namely Brake by Wire from Volvo Group Trucks Technology, Sweden. 

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-42803 (URN)10.1145/3297280.3297493 (DOI)2-s2.0-85065663281 (Scopus ID)
Conference
SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019
Available from: 2019-02-27 Created: 2019-02-27 Last updated: 2019-05-24Bibliographically approved
Filipovikj, P. & Seceleanu, C. (2019). Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners. In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019: . Paper presented at ENASE 2019: 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, Crete, Greece, May 4, 2019 - May 5, 2019 (pp. 92-103).
Open this publication in new window or tab >>Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners
2019 (English)In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019, 2019, p. 92-103Conference paper, Published paper (Refereed)
Abstract [en]

With the ever-increasing size and complexity of the industrial software systems there is an imperative need for an automated, systematic and exhaustive verification of various software artifacts, such as system specifications, models, code, etc. A potential remedy for this need might lie in a pool of techniques for computer-aided verification of software related artifacts, including system specifications. The Achilles' heel of these techniques, and the main hinder for their wider adoption in industrial development process are the complexity and the specialized skill-set required for the formal encoding of specifications. To alleviate this problem, Specification Patterns that are based on the observation that the system specifications are framed within reoccurring solutions have been proposed. The approach has been shown to be expressive enough for capturing requirements in the automotive domain, however, there is a lack of empirical data that can be used to judge its practical usefulness. In this paper, we involve an existing specification-patterns-based tool, and propose a small-size evaluation of the approach with practitioners, on a case study conducted in cooperation with Scania, one of the world's leading manufacturers of heavy-load vehicles. Our results show that the specification patterns that are supported by an adequate tooling have the potential for adoption in industrial practice. 

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-42802 (URN)2-s2.0-85067481667 (Scopus ID)9789897583759 (ISBN)
Conference
ENASE 2019: 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, Crete, Greece, May 4, 2019 - May 5, 2019
Available from: 2019-02-27 Created: 2019-02-27 Last updated: 2019-06-27Bibliographically approved
Filipovikj, P. & Seceleanu, C. (2019). Specifying industrial system requirements using specification patterns: A case study of evaluation with practitioners. In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering: . Paper presented at 14th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2019, 4 May 2019 through 5 May 2019 (pp. 92-103). SciTePress
Open this publication in new window or tab >>Specifying industrial system requirements using specification patterns: A case study of evaluation with practitioners
2019 (English)In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering, SciTePress , 2019, p. 92-103Conference paper, Published paper (Refereed)
Abstract [en]

With the ever-increasing size and complexity of the industrial software systems there is an imperative need for an automated, systematic and exhaustive verification of various software artifacts, such as system specifications, models, code, etc. A potential remedy for this need might lie in a pool of techniques for computer-aided verification of software related artifacts, including system specifications. The Achilles' heel of these techniques, and the main hinder for their wider adoption in the industrial development process are the complexity and the specialized skill-set required for the formal encoding of specifications. To alleviate this problem, Specification Patterns that are based on the observation that the system specifications are framed within reoccurring solutions have been proposed. The approach has been shown to be expressive enough for capturing requirements in the automotive domain, however, there is a lack of empirical data that can be used to judge its practical usefulness. In this paper, we involve an existing specification-patterns-based tool, called PROPAS, and propose a small-size evaluation of the approach with practitioners, on a case study conducted in cooperation with Scania, Sweden, one of the world's leading manufacturers of heavy-load vehicles. Our results show that the specification patterns that are supported by an adequate tooling have the potential to be practically usefull for the non-experts in formal methods.

Place, publisher, year, edition, pages
SciTePress, 2019
Keywords
Industrial Case Study, Pattern-Based Requirements Specification, Specification Patterns, Automobile manufacture, Computer aided analysis, Computer software selection and evaluation, Formal verification, Computer aided verifications, Heavy-load vehicles, Industrial development, Industrial software, Requirements specifications, System specification, Formal specification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-44881 (URN)2-s2.0-85067481667 (Scopus ID)9789897583759 (ISBN)
Conference
14th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2019, 4 May 2019 through 5 May 2019
Available from: 2019-07-11 Created: 2019-07-11 Last updated: 2019-07-11Bibliographically approved
Cai, S., Gallina, B., Nyström, D. & Seceleanu, C. (2019). Statistical Model Checking for Real-Time Database Management Systems: A Case Study. In: The 24th IEEE Conference on Emerging Technologies and Factory Automation ETFA2019: . Paper presented at The 24th IEEE Conference on Emerging Technologies and Factory Automation ETFA2019, 10 Sep 2019, Zaragoza, Spain.
Open this publication in new window or tab >>Statistical Model Checking for Real-Time Database Management Systems: A Case Study
2019 (English)In: The 24th IEEE Conference on Emerging Technologies and Factory Automation ETFA2019, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Many industrial control systems manage critical data using Database Management Systems (DBMS). The correctness of transactions, especially their atomicity, isolation and temporal correctness, is essential for the dependability of the entire system. Existing methods and techniques, however, either lack the ability to analyze the interplay of these properties, or do not scale well for systems with large amounts of transactions and data, and complex transaction management mechanisms. In this paper, we propose to analyze large scale real-time database systems using statistical model checking. We propose a pattern-based framework, by extending our previous work, to model the real-time DBMS as a network of stochastic timed automata, which can be analyzed by UPPAAL Statistical Model Checker. We present an industrial case study, in which we design a collision avoidance system for multiple autonomous construction vehicles, via concurrency control of a real-time DBMS. The desired properties of the designed system are analyzed using our proposed framework.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-45045 (URN)
Conference
The 24th IEEE Conference on Emerging Technologies and Factory Automation ETFA2019, 10 Sep 2019, Zaragoza, Spain
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2019-08-22 Created: 2019-08-22 Last updated: 2019-08-22Bibliographically approved
Cai, S., Gallina, B., Nyström, D., Seceleanu, C. & Larsson, A. (2019). Tool-supported design of data aggregation processes in cloud monitoring systems. Journal of Ambient Intelligence and Humanized Computing, 10(7), 2519-2535
Open this publication in new window or tab >>Tool-supported design of data aggregation processes in cloud monitoring systems
Show others...
2019 (English)In: Journal of Ambient Intelligence and Humanized Computing, ISSN 1868-5137, E-ISSN 1868-5145, Vol. 10, no 7, p. 2519-2535Article in journal (Refereed) Published
Abstract [en]

Efficient monitoring of a cloud system involves multiple aggregation processes and large amounts of data with various and interdependent requirements. A thorough understanding and analysis of the characteristics of data aggregation processes can help to improve the software quality and reduce development cost. In this paper, we propose a systematic approach for designing data aggregation processes in cloud monitoring systems. Our approach applies a feature-oriented taxonomy called DAGGTAX (Data AGGregation TAXonomy) to systematically specify the features of the designed system, and SAT-based analysis to check the consistency of the specifications. Following our approach, designers first specify the data aggregation processes by selecting and composing the features from DAGGTAX. These specified features, as well as design constraints, are then formalized as propositional formulas, whose consistency is checked by the Z3 SAT solver. To support our approach, we propose a design tool called SAFARE (SAt-based Feature-oriented dAta aggREgation design), which implements DAGGTAX-based specification of data aggregation processes and design constraints, and integrates the state-of-the-art solver Z3 for automated analysis. We also propose a set of general design constraints, which are integrated by default in SAFARE. The effectiveness of our approach is demonstrated via a case study provided by industry, which aims to design a cloud monitoring system for video streaming. The case study shows that DAGGTAX and SAFARE can help designers to identify reusable features, eliminate infeasible design decisions, and derive crucial system parameters.

Place, publisher, year, edition, pages
Springer Verlag, 2019
Keywords
Cloud monitoring system design, Consistency checking, Data aggregation, Feature model, Computer software selection and evaluation, Design, Quality control, Specifications, Taxonomies, Based specification, Cloud monitoring, Efficient monitoring, Feature modeling, Large amounts of data, Propositional formulas, Monitoring
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-43881 (URN)10.1007/s12652-018-0730-6 (DOI)000469922500004 ()2-s2.0-85049591829 (Scopus ID)
Available from: 2019-06-11 Created: 2019-06-11 Last updated: 2019-06-18Bibliographically approved
Gu, R., Marinescu, R., Seceleanu, C. & Lundqvist, K. (2019). Towards a Two-layer Framework for Verifying Autonomous Vehicles. In: NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460: . Paper presented at 11th Annual NASA Formal Methods Symposium NFM 2019, 07 May 2019, Houston, United States.
Open this publication in new window or tab >>Towards a Two-layer Framework for Verifying Autonomous Vehicles
2019 (English)In: NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Autonomous vehicles rely heavily on intelligent algorithms for path planning and collision avoidance, and their functionality and dependability could be ensured through formal verification. To facilitate the verification, it is beneficial to decouple the static high-level planning from the dynamic functions like collision avoidance. In this paper, we propose a conceptual two-layer framework for verifying autonomous vehicles, which consists of a static layer and a dynamic layer. We focus concretely on modeling and verifying the dynamic layer using hybrid automata and UPPAAL SMC, where a continuous movement of the vehicle as well as collision avoidance via a dipole flow field algorithm are considered. This framework achieves decoupling by separating the verification of the vehicle's autonomous path planning from that of the vehicle autonomous operation in a continuous dynamic environment. To simplify the modeling process, we propose a pattern-based design method, where patterns are expressed as hybrid automata. We demonstrate the applicability of the dynamic layer of our framework on an industrial prototype of an autonomous wheel loader.

Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 11460
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-43924 (URN)10.1007/978-3-030-20652-9_12 (DOI)2-s2.0-85066869584 (Scopus ID)9783030206512 (ISBN)
Conference
11th Annual NASA Formal Methods Symposium NFM 2019, 07 May 2019, Houston, United States
Projects
DPAC - Dependable Platforms for Autonomous systems and Control
Available from: 2019-06-19 Created: 2019-06-19 Last updated: 2019-06-20Bibliographically approved
Awada, I. A., Cramariuc, O., Mocanu, I., Seceleanu, C., Kunnappilly, A. & Florea, A. M. (2018). An end- user perspective on the CAMI Ambient and Assisted Living Project. In: INTED2018 Proceedings: . Paper presented at 12th annual International Technology, Education and Development Conference INTED 2018, 05 Mar 2018, Valencia, Spain.
Open this publication in new window or tab >>An end- user perspective on the CAMI Ambient and Assisted Living Project
Show others...
2018 (English)In: INTED2018 Proceedings, 2018Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we present the outcomes and conclusions obtained by involving seniors from three countries (Denmark, Poland and Romania) in an innovative project funded under the European Ambient Assisted Living (ALL) program. CAMI stands for "Companion with Autonomously Mobile Interface" in "Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL". The CAMI solution enables flexible, scalable and individualised services that support elderly to self-manage their daily life and prolong their involvement in the society (sharing knowledge, continue working, etc). This also allows their informal caregivers (family and friends) to continue working and participating in society while caring for their loved ones. The solution is designed as an innovative architecture that allows for individualized, intelligent self-management which can be tailored to an individual's preferences and needs. A user-centred approach has ranked health monitoring, computer supervised physical exercises and voice based interaction among the top favoured CAMI functionalities. Respondents from three countries (Poland, Romania and Denmark) participated in a multinational survey and a conjoint analysis study.

Keywords
user-centred design, artificial intelligence, fall detection, exergames, vocal interface
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-38958 (URN)10.21125/inted.2018.1596 (DOI)000448704001118 ()978-84-697-9480-7 (ISBN)
Conference
12th annual International Technology, Education and Development Conference INTED 2018, 05 Mar 2018, Valencia, Spain
Projects
CAMI - Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL (Ambient Assisted Living)
Available from: 2018-05-15 Created: 2018-05-15 Last updated: 2019-03-14Bibliographically approved
Kunnappilly, A., Marinescu, R. & Seceleanu, C. (2018). Assuring intelligent ambient assisted living solutions by statistical model checking. In: Lect. Notes Comput. Sci.: . Paper presented at 5 November 2018 through 9 November 2018 (pp. 457-476). Springer Verlag
Open this publication in new window or tab >>Assuring intelligent ambient assisted living solutions by statistical model checking
2018 (English)In: Lect. Notes Comput. Sci., Springer Verlag , 2018, p. 457-476Conference paper, Published paper (Refereed)
Abstract [en]

A modern way of enhancing elderly people’s quality of life is by employing various Ambient Assisted Living solutions that facilitate an independent and safe living for their users. This is achieved by integrating computerized functions such as health and home monitoring, fall detection, reminders, etc. Such systems are safety critical, therefore ensuring at design time that they operate correctly, but also in a timely and robust manner is important. Most of the solutions are not analyzed formally at design time, especially if such Ambient Assisted Living functions are integrated within the same design. To address this concern, we propose a framework that relies on an abstract component-based description of the system’s architecture in the Architecture Analysis and Design Language. To ensure scalability of analysis, we transform the AADL models into a network of stochastic timed automata amenable to statistical analysis of various quality-of-service attributes. The architecture that we analyze is developed as part of the project CAMI, co-financed by the European Commission, and consists of a variety of health and home sensors, a data collector, local and cloud processing, as well as an artificial-intelligence-based decision support system. Our contribution paves the way towards achieving design-time assured integrated Ambient Assisted Living solutions, which in turn could reduce verification effort at later stages.

Place, publisher, year, edition, pages
Springer Verlag, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 11245 LNCS
Keywords
Artificial intelligence, Computer architecture, Decision support systems, Formal methods, Model checking, Network architecture, Quality control, Quality of service, Safety engineering, Stochastic models, Stochastic systems, Ambient assisted living, Architecture analysis, Cloud processing, Component based, Design languages, European Commission, Home monitoring, Statistical model checking, Assisted living
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-41449 (URN)10.1007/978-3-030-03421-4_29 (DOI)2-s2.0-85056457127 (Scopus ID)9783030034207 (ISBN)
Conference
5 November 2018 through 9 November 2018
Available from: 2018-11-29 Created: 2018-11-29 Last updated: 2019-03-14Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-2870-2680

Search in DiVA

Show all publications