mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Alternative names
Publications (10 of 97) Show all publications
Filipovikj, P., Rodriguez-Navas, G. & Seceleanu, C. (2019). Bounded Invariance Checking of Simulink Models. In: : . Paper presented at SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019 (pp. 2168-2178).
Open this publication in new window or tab >>Bounded Invariance Checking of Simulink Models
2019 (English)Conference 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)
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-02-27Bibliographically 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
Cai, S., Gallina, B., Nyström, D. & Seceleanu, C. (2018). Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems. In: 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018: . Paper presented at 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018, 30 Oct 2018, Limassol, Cyprus (pp. 355-374).
Open this publication in new window or tab >>Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems
2018 (English)In: 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018, 2018, p. 355-374Conference paper, Published paper (Refereed)
Abstract [en]

Concurrency control faults may lead to unwanted interleavings, and breach data consistency in distributed transaction systems. However, due to the unpredictable delays between sites, detecting concurrency control faults in distributed transaction systems is difficult. In this paper, we propose a methodology, relying on model-based testing and mutation testing, for designing test cases in order to detect such faults. The generated test inputs are designated delays between distributed operations, while the outputs are the occurrence of unwanted interleavings that are consequences of the concurrency control faults. We mutate the distributed transaction specification with common concurrency control faults, and model them as UPPAAL timed automata, in which designated delays are encoded as stopwatches. Test cases are generated via reachability analysis using UPPAAL Model Checker, and are selected to form an effective test suite. Our methodology can reduce redundant test cases, and find the appropriate delays to detect concurrency control faults effectively.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41709 (URN)10.1007/978-3-030-03424-5_24 (DOI)978-3-030-03424-5 (ISBN)
Conference
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018, 30 Oct 2018, Limassol, Cyprus
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2018-12-20 Created: 2018-12-20 Last updated: 2018-12-20Bibliographically approved
Gu, R., Marinescu, R., Seceleanu, C. & Lundqvist, K. (2018). Formal verification of an Autonomous Wheel Loader by model checking. In: Proceedings - International Conference on Software Engineering: . Paper presented at 6th ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018, co-located with International Conference on Software Engineering, ICSE 2018, 2 June 2018 (pp. 74-83). IEEE Computer Society
Open this publication in new window or tab >>Formal verification of an Autonomous Wheel Loader by model checking
2018 (English)In: Proceedings - International Conference on Software Engineering, IEEE Computer Society , 2018, p. 74-83Conference paper, Published paper (Refereed)
Abstract [en]

In an attempt to increase productivity and the workers' safety, the construction industry is moving towards autonomous construction sites, where various construction machines operate without human intervention. In order to perform their tasks autonomously, the machines are equipped with different features, such as position localization, human and obstacle detection, collision avoidance, etc. Such systems are safety critical, and should operate autonomously with very high dependability (e.g., by meeting task deadlines, avoiding (fatal) accidents at all costs, etc.). An Autonomous Wheel Loader is a machine that transports materials within the construction site without a human in the cab. To check the dependability of the loader, in this paper we provide a timed automata description of the vehicle's control system, including the abstracted path planning and collision avoidance algorithms used to navigate the loader, and we model check the encoding in UPPAAL, against various functional, timing and safety requirements. The complex nature of the navigation algorithms makes the loader's abstract modeling and the verification very challenging. Our work shows that exhaustive verification techniques can be applied early in the development of autonomous systems, to enable finding potential design errors that would incur increased costs if discovered later.

Place, publisher, year, edition, pages
IEEE Computer Society, 2018
Keywords
Autonomous Vehicle, Collision Avoidance, Formal Verification, Model Checking, Timed Automata, UPPAAL, Accident prevention, Automata theory, Construction equipment, Construction industry, Loaders, Mining machinery, Motion planning, Obstacle detectors, Wheels, Autonomous constructions, Autonomous Vehicles, Construction machines, Navigation algorithms, Safety requirements, Verification techniques
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-40747 (URN)10.1145/3193992.3193999 (DOI)2-s2.0-85052130860 (Scopus ID)9781450357180 (ISBN)
Conference
6th ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018, co-located with International Conference on Software Engineering, ICSE 2018, 2 June 2018
Available from: 2018-09-07 Created: 2018-09-07 Last updated: 2018-09-07Bibliographically approved
Cavalcanti, A., Petrucci, L. & Seceleanu, C. (2018). Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems. ERCIM News (112), 47-47
Open this publication in new window or tab >>Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems
2018 (English)In: ERCIM News, ISSN 0926-4981, E-ISSN 1564-0094, no 112, p. 47-47Article in journal, Editorial material (Other academic) Published
Abstract [en]

The yearly workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS) was organised as a joint event together with the workshop on Automated Verification of Critical Systems (AVoCS). The resulting FMICS-AVoCS 2017 workshop took place on 18-20 September in Turin, hosted by the University of Turin.

Place, publisher, year, edition, pages
EUROPEAN RESEARCH CONSORTIUM INFORMATICS & MATHEMATICS, 2018
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-39206 (URN)000430463000027 ()
Available from: 2018-05-11 Created: 2018-05-11 Last updated: 2018-05-11Bibliographically approved
Filipovikj, P., Rodriguez-Navas, G. & Seceleanu, C. (2018). Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience. Electronic Communications of the EASST, 75, 1-20
Open this publication in new window or tab >>Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience
2018 (English)In: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 75, p. 1-20Article in journal (Refereed) Published
Abstract [en]

Industry relies predominantly on manual peer-review techniques for assessing the correctness of system specifications. However, with the ever-increasing size, complexity and intricacy of specifications, it becomes difficult to assure their correctness with respect to certain criteria such as consistency. To address this challenge, a technique called sanity checking has been proposed. The goal of the technique is to assess the quality of the system specification in a systematic and rigorous manner with respect to a formally-defined criterion. Predominantly, the sanity checking criteria, such as for instance consistency, are encoded as reachability or liveness properties which can then be verified via model checking. Recently, a complementary approach for checking the consistency of a system's specification by reducing it to a satisfiability problem that can be analyzed using Satisfiability Modulo Theories has been proposed. In this paper, we compare the two approaches for consistency analysis, by applying them on a relevant industrial use case, using the same definition for consistency and the same set of requirements. Since the bottlenecks of analyzing large systems formally are most often the construction of the model and the time needed to return a verdict, we carry out the comparison with respect to the: i) required effort for generating the analysis model and the latter's complexity, and ii) consistency analysis time. Assuming checking only invariance properties, our results show no significant difference in analysis time between the two approaches when applied on the same system specification under the same definition of consistency. As expected, the main difference between the two comes from the required time and effort of creating the analysis models.

Place, publisher, year, edition, pages
Germany: , 2018
Keywords
SMT-based consistency analysis, model-checking-based consistency analysis
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41726 (URN)10.14279/tuj.eceasst.75 (DOI)ISSN 1863-2122 (ISBN)
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2018-12-20 Created: 2018-12-20 Last updated: 2018-12-20Bibliographically approved
Cai, S., Gallina, B., Nyström, D. & Seceleanu, C. (2018). Specification and Formal Verification of Atomic Concurrent Real-Time Transactions. In: 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018: . Paper presented at The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 04 Dec 2018, Taipei, Taiwan.
Open this publication in new window or tab >>Specification and Formal Verification of Atomic Concurrent Real-Time Transactions
2018 (English)In: 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 2018Conference paper, Published paper (Refereed)
Abstract [en]

Although atomicity, isolation and temporal correctness are crucial to the dependability of many real-time database-centric systems, the selected assurance mechanism for one property may breach another. Trading off these properties requires to specify and analyze their dependencies, together with the selected supporting mechanisms (abort recovery, concurrency control, and scheduling), which is still insufficiently supported. In this paper, we propose a UML profile, called UTRAN, for specifying atomic concurrent real-time transactions, with explicit support for all three properties and their supporting mechanisms. We also propose a pattern-based modeling framework, called UPPCART, to formalize the transactions and the mechanisms specified in UTRAN, as UPPAAL timed automata. Various mechanisms can be modeled flexibly using our reusable patterns, after which the desired properties can be verified by the UPPAAL model checker. Our techniques facilitate systematic analysis of atomicity, isolation and temporal correctness trade-offs with guarantee, thus contributing to a dependable real-time database system.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41710 (URN)000462280800012 ()978-1-5386-5700-3 (ISBN)
Conference
The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 04 Dec 2018, Taipei, Taiwan
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2018-12-18 Created: 2018-12-18 Last updated: 2019-04-11Bibliographically approved
Kunnappilly, A., Sorici, A., Awada, I. A., Mocanu, I., Seceleanu, C. & Florea, A. M. (2017). A Novel Integrated Architecture for Ambient Assisted Living Systems. In: The 41st IEEE Computer Society International Conference on Computers, Software & Applications COMPSAC 2017: . Paper presented at The 41st IEEE Computer Society International Conference on Computers, Software & Applications COMPSAC 2017, 04 Jul 2017, Turin, Italy (pp. 465-472). , 1, Article ID 8029645.
Open this publication in new window or tab >>A Novel Integrated Architecture for Ambient Assisted Living Systems
Show others...
2017 (English)In: The 41st IEEE Computer Society International Conference on Computers, Software & Applications COMPSAC 2017, 2017, Vol. 1, p. 465-472, article id 8029645Conference paper, Published paper (Refereed)
Abstract [en]

The increase in life expectancy and the slumping birth rates across the world result in lengthening the average age of the society. This change in demography has many consequences, the major being the insufficient number of caregivers. Therefore, we are in need of techniques that will assist the elderly in their daily life, while preventing their social isolation. The recent developments in Ambient Intelligence (AmI) and Information and Communication Technologies (ICT) have facilitated a technological revolution in the field of Ambient Assisted Living (AAL). At present, there are many technologies on the market that support the independent life of older adults, requiring less assistance from family and caregivers, yet most of them offer isolated services, such as health monitoring, supervised exercises, reminders etc. There are only very few architectures that support the seamless integration of various functionalities and none of them incorporates user preferences or are formally analyzed for their functionality and quality-of-service attributes which is needed in order to ensure safe mitigations of potential critical scenarios. In this paper, we propose a novel architectural solution that seamlessly integrates necessary functions of an AAL system, based on user preferences. To enable a first level of the architecture's analysis, we model our system in Architecture Analysis and Design Language (AADL), and carry out its simulation for analyzing the end-to-end data-flow latency, resource budgets and system safety.

Keywords
Ambient Intelligence, Ambient Assisted Living, Architecture Analysis and Design Language.
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-35500 (URN)10.1109/COMPSAC.2017.28 (DOI)000424861400061 ()2-s2.0-85031918944 (Scopus ID)
Conference
The 41st IEEE Computer Society International Conference on Computers, Software & Applications COMPSAC 2017, 04 Jul 2017, Turin, Italy
Projects
CAMI - Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL (Ambient Assisted Living)
Available from: 2017-06-09 Created: 2017-06-09 Last updated: 2019-03-14Bibliographically approved
Marinescu, R., Filipovikj, P., Enoiu, E. P., Larsson, J. & Seceleanu, C. (2017). An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models. In: 29th Nordic Workshop on Programming Theory NWPT'17: . Paper presented at 29th Nordic Workshop on Programming Theory NWPT'17, 01 Nov 2017, Turku, Finland , Finland (pp. 40-43). Turku, Finland , Finland: TUCS Lecture Notes
Open this publication in new window or tab >>An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models
Show others...
2017 (English)In: 29th Nordic Workshop on Programming Theory NWPT'17, Turku, Finland , Finland: TUCS Lecture Notes , 2017, p. 40-43Conference paper, Published paper (Refereed)
Abstract [en]

Early design artifacts of embedded systems, such as architectural models, represent convenient abstractions for reasoning about a system’s structure and functionality. One such example is the Electronic Architecture and Software Tools-Architecture Description Language (EAST-ADL), a domain-specific architectural language that targets the automotive industry. EAST-ADL is used to represent both hardware and software elements, as well as related extra-functional information (e.g., timing properties, triggering information, resource consumption). Testing architectural models is an important activity in engineering large-scale industrial systems, which sparks a growing research interest. Modern embedded systems, such as autonomous vehicles and robots, have low-energy computing demands, making testing for energy usage increasingly important. Nevertheless, testing resource-aware properties of architectural models has received less attention than the functional testing of such models. In our previous work, we have outlined a method for testing energy consumption in embedded systems using manually created faults based on statistical model checking of a priced formal system model. In this paper, we extend our previous work by showing how mutation testing] can be used to generate and select test cases based on the concept of energy-aware mutants– small syntactic modifications in the architectural model, intended to mimic real energy faults. Test cases that can distinguish a certain behavior from its mutations are sensitive to changes in the model, and hence considered to be good at detecting faults. The main contributions of this paper are: (i) an approach for creating energy-related mutants for EAST-ADL architectural models, (ii) a method for overcoming the equivalent mutant problem (i.e., the problem of finding a test case which can distinguish the observable behavior of a mutant from the original one), (iii) a test generation approach based on UPPAAL Statistical Model Checker (SMC), and (iv) a test selection criteria based on mutation analysis using our MATS tool.

Place, publisher, year, edition, pages
Turku, Finland , Finland: TUCS Lecture Notes, 2017
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-37338 (URN)978-952-12-3608-2 (ISBN)
Conference
29th Nordic Workshop on Programming Theory NWPT'17, 01 Nov 2017, Turku, Finland , Finland
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyCAMI - Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL (Ambient Assisted Living)DPAC - Dependable Platforms for Autonomous systems and ControlMegaMaRt2 - Megamodelling at Runtime (ECSEL/Vinnova)
Available from: 2017-11-28 Created: 2017-11-28 Last updated: 2018-10-31Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-2870-2680

Search in DiVA

Show all publications