mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Alternative names
Publications (10 of 108) 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
Kunnappilly, A., Marinescu, R. & Seceleanu, C. (2019). A Model-Checking-Based Framework for Analyzing Ambient Assisted Living Solutions. Sensors, 19(22)
Open this publication in new window or tab >>A Model-Checking-Based Framework for Analyzing Ambient Assisted Living Solutions
2019 (English)In: Sensors, ISSN 1424-8220, E-ISSN 1424-8220, Vol. 19, no 22Article in journal (Refereed) Published
Abstract [en]

Since modern ambient assisted living solutions integrate a multitude of assisted-living functionalities, out of which some are safety critical, it is desirable that these systems are analyzed 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 collection, local and cloud processing schemes, and an intelligent decision support system, which can be easily extended to suit specific architecture categories. Our solution is customizable, therefore, we show three instantiations of the generic model, as simple, intermediate, and complex configurations, 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, which can also account for the probabilistic behavior of such systems, and captures the possibility of component failure. To enable formal analysis, we describe the semantics of the simple and complex architectures within the framework of timed automata. We show that the simple architecture is amenable to exhaustive model checking by employing the UPPAAL tool, whereas for the complex architecture we resort to statistical model checking for scalability reasons. In this case, we apply the statistical extension of UPPAAL, namely UPPAAL SMC. Our work paves the way for the development of formally assured future ambient assisted living solutions.

Place, publisher, year, edition, pages
NLM (Medline), 2019
Keywords
ambient assisted living, Architecture Analysis and Design Language, statistical model checking, UPPAAL SMC
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-46214 (URN)10.3390/s19225057 (DOI)000503381500235 ()2-s2.0-85075442718 (Scopus ID)
Available from: 2019-12-02 Created: 2019-12-02 Last updated: 2020-01-09Bibliographically 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)000474685800302 ()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-10-11Bibliographically approved
Cai, S., Gallina, B., Nyström, D. & Seceleanu, C. (2019). Data Aggregation Processes: A Survey, A Taxonomy, and Design Guidelines. Computing, 101(10), 1397-1429
Open this publication in new window or tab >>Data Aggregation Processes: A Survey, A Taxonomy, and Design Guidelines
2019 (English)In: Computing, ISSN 0010-485X, E-ISSN 1436-5057, Vol. 101, no 10, p. 1397-1429Article in journal (Refereed) Published
Abstract [en]

Data aggregation processes are essential constituents for data management in modern computer systems, such as decision support systems and Internet of Things (IoT) systems, many with timing constraints. Understanding the common and variable features of data aggregation processes, especially their implications to the timerelated properties, is key to improving the quality of the designed system and reduce design effort. In this paper, we present a survey of data aggregation processes in a variety of application domains from literature.We investigate their common and variable features, which serves as the basis of our previously proposed taxonomy called DAGGTAX. By studying the implications of the DAGGTAX features, we formulate a set of constraints to be satisfied during design, which helps to check the correctness of the specifications and reduce the design space. We also provide a set of design heuristics that could help designers to decide the appropriate mechanisms for achieving the selected features. We apply DAGGTAX on industrial case studies, showing that DAGGTAX not only strengthens the understanding, but also serves as the foundation of a design tool which facilitates the model-driven design of data aggregation processes.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41747 (URN)10.1007/s00607-018-0679-5 (DOI)000487922400002 ()2-s2.0-85056698473 (Scopus ID)
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2018-12-18 Created: 2018-12-18 Last updated: 2019-12-12Bibliographically approved
Salimi, M., Majd, A., Loni, M., Seceleanu, T., Seceleanu, C., Sirjani, M., . . . Troubitsyna, E. (2019). Multi-objective optimization of real-time task scheduling problem for distributed environments. In: ACM International Conference Proceeding Series: . Paper presented at 6th Conference on the Engineering of Computer-Based Systems, ECBS 2019, 2 September 2019 through 3 September 2019. Association for Computing Machinery, Article ID a13.
Open this publication in new window or tab >>Multi-objective optimization of real-time task scheduling problem for distributed environments
Show others...
2019 (English)In: ACM International Conference Proceeding Series, Association for Computing Machinery , 2019, article id a13Conference paper, Published paper (Refereed)
Abstract [en]

Real-world applications are composed of multiple tasks which usually have intricate data dependencies. To exploit distributed processing platforms, task allocation and scheduling, that is assigning tasks to processing units and ordering inter-processing unit data transfers, plays a vital role. However, optimally scheduling tasks on processing units and finding an optimized network topology is an NP-complete problem. The problem becomes more complicated when the tasks have real-time deadlines for termination. Exploring the whole search space in order to find the optimal solution is not feasible in a reasonable amount of time, therefore meta-heuristics are often used to find a near-optimal solution. We propose here a multi-population evolutionary approach for near-optimal scheduling optimization, that guarantees end-to-end deadlines of tasks in distributed processing environments. We analyze two different exploration scenarios including single and multi-objective exploration. The main goal of the single objective exploration algorithm is to achieve the minimal number of processing units for all the tasks, whereas a multi-objective optimization tries to optimize two conflicting objectives simultaneously considering the total number of processing units and end-to-end finishing time for all the jobs. The potential of the proposed approach is demonstrated by experiments based on a use case for mapping a number of jobs covering industrial automation systems, where each of the jobs consists of a number of tasks in a distributed environment.

Place, publisher, year, edition, pages
Association for Computing Machinery, 2019
Keywords
Distributed Task Scheduling, Evolutionary Computing, Multi-Objective Optimization, Real-Time Processing, Automation, Computational complexity, Data handling, Data transfer, Finishing, Image coding, Job shop scheduling, Multitasking, Optimal systems, Scheduling, Scheduling algorithms, Conflicting objectives, Distributed environments, Distributed processing, Distributed tasks, Industrial automation system, Realtime processing, Task allocation and scheduling, Multiobjective optimization
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-46527 (URN)10.1145/3352700.3352713 (DOI)2-s2.0-85075887884 (Scopus ID)9781450376365 (ISBN)
Conference
6th Conference on the Engineering of Computer-Based Systems, ECBS 2019, 2 September 2019 through 3 September 2019
Available from: 2019-12-17 Created: 2019-12-17 Last updated: 2019-12-19Bibliographically approved
Cai, S., Gallina, B., Nyström, D. & Seceleanu, C. (2019). Specification and Automated Verification of Atomic Concurrent Real-Time Transactions.
Open this publication in new window or tab >>Specification and Automated Verification of Atomic Concurrent Real-Time Transactions
2019 (English)Manuscript (preprint) (Other academic)
National Category
Software Engineering
Identifiers
urn:nbn:se:mdh:diva-45212 (URN)
Available from: 2019-09-13 Created: 2019-09-13 Last updated: 2019-09-20Bibliographically 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
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 (pp. 306-313).
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, 2019, p. 306-313Conference 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)10.1109/ETFA.2019.8869326 (DOI)2-s2.0-85074192007 (Scopus ID)
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-12-18Bibliographically approved
Foughali, M., Ingrand, F. & Seceleanu, C. (2019). Statistical Model Checking of Complex Robotic Systems. In: Lect. Notes Comput. Sci.: . Paper presented at 15 July 2019 through 16 July 2019 (pp. 114-134). Springer
Open this publication in new window or tab >>Statistical Model Checking of Complex Robotic Systems
2019 (English)In: Lect. Notes Comput. Sci., Springer , 2019, p. 114-134Conference paper, Published paper (Refereed)
Abstract [en]

Failure of robotic software may cause catastrophic damages. In order to establish a higher level of trust in robotic systems, formal methods are often proposed. However, their applicability to the functional layer of robots remains limited because of the informal nature of specifications, their complexity and size. In this paper, we formalize the robotic framework and automatically translate its components to UPPAAL-SMC, a real-time statistical model checker. We apply our approach to verify properties of interest on a real-world autonomous drone navigation that does not scale with regular UPPAAL.

Place, publisher, year, edition, pages
Springer, 2019
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 11636 LNCS
Keywords
Air navigation, Drones, Formal methods, Robotics, Robots, Catastrophic damage, Functional layer, Real-world, Robotic softwares, Robotic systems, Statistical model checking, Statistical modeling, Uppaal-smc, Model checking
National Category
Energy Engineering
Identifiers
urn:nbn:se:mdh:diva-46548 (URN)10.1007/978-3-030-30923-7_7 (DOI)2-s2.0-85075579856 (Scopus ID)9783030309220 (ISBN)
Conference
15 July 2019 through 16 July 2019
Available from: 2019-12-16 Created: 2019-12-16 Last updated: 2019-12-16Bibliographically 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-09-13Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-2870-2680

Search in DiVA

Show all publications