https://www.mdu.se/

mdu.sePublications
Change search
Refine search result
123 1 - 50 of 144
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Awada, Imad Alex
    et al.
    University Politehnica of Bucharest, Romania.
    Cramariuc, Oana
    IT Cenetr for Science and Technology, Romania.
    Mocanu, Irina
    University Politehnica of Bucharest.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Kunnappilly, Ashalatha
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Florea, Adina Magda
    University Politehnica of Bucharest, Romania.
    An end- user perspective on the CAMI Ambient and Assisted Living Project2018In: INTED2018 Proceedings, 2018, p. 6776-6785Conference 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.

  • 2.
    Back, Ralph-Johan
    et al.
    Turku Centre for Computer Science .
    Cerschi (Seceleanu), Cristina
    Turku Centre for Computer Science .
    Modeling and Verifying a Temperature Control System using Continuous Action Systems2000Conference paper (Refereed)
    Abstract [en]

    We formally describe and verify a real-time temperature control system for a nuclear reactor tank, using a generalization of action systems to hybrid systems (based on weakest precondition predicate transformer semantics) as our formal framework. The analyzed control system is a linear hybrid system, combining discrete control with continuous dynamics. Our work can be seen as a case study on the applicability of the hybrid action system formalism to study the reachability problem, i.e., to prove that an unsafe state can not be reached by executing the system.

  • 3.
    Back, Ralph-Johan
    et al.
    Åbo Akademi University.
    Seceleanu, Cristina
    Åbo Akademi University.
    Contracts and Games in Controller Synthesis for Discrete Systems2004In: Proceedings - 11th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2004, 2004, p. 307-314Conference paper (Refereed)
    Abstract [en]

    This study proposes a method for constructing reliable controllers for arbitrarily large discrete systems. The controller is synthesized by finding a winning strategy for specific games defined by contracts. The discrete system model is an action system, and the requirement is a temporal property. We use the extended action system notation that allows both angelic and demonic nondeterminism, such that the game reduces to a competition between the angel, that is, the controller, and the demon, that is, the plant, which try to prevent each other from achieving their respective goals. If the synthesis is possible, that is, if the angel has a way to enforce the required property, the process ends with finding the winning strategy of the angel, by propagating backwards the computed precondition of the demon, with respect to that property. This technique guarantees the correctness of the derived program. We illustrate our method on a producer-consumer application.

  • 4.
    Back, Ralph-Johan
    et al.
    Turku Centre for Computer Science, Finland.
    Seceleanu, Cristina
    Turku Centre for Computer Science, Finland.
    Westerholm, Jan
    Turku Centre for Computer Science, Finland.
    Symbolic Simulation of Hybrid Systems2002Conference paper (Refereed)
    Abstract [en]

    Continuous action systems (CAS) is a formalism intended for modeling hybrid systems (systems that combine discrete control with continuous behavior), and proving properties about the model within refinement calculus. In this paper we use a symbolic manipulation program to build a tool for simulating CAS models by calculating symbolically the time evolution of the discrete and continuous CAS model functions, as explicit and exact expressions of a continuous time variable. We may then study the time behavior and general properties of the model by plotting these functions with respect to time. For certain models our tool eliminates the need for introducing tolerances into the model structure. The tool is useful for checking that the model behaves correctly, and we can sometimes study the behavior of CAS models with in principle infinite precision.

  • 5.
    Backeman, Peter
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Innovation and Product Realisation.
    Kunnappilly, A.
    Alstom, Västerås, Sweden.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Supporting 5G Service Orchestration with Formal Verification2023In: Computer Science and Information Systems, ISSN 1820-0214, Vol. 29, no 1, p. 329-357Article in journal (Refereed)
    Abstract [en]

    The 5G communication technology has the ability to create logical net-works, called network slices, which are specifically carved to serve particular application domains. Due to the mix of different application criticality, it becomes crucial to verify if the applications’ service level agreements are met. In this pa-per, we propose a novel framework for modeling and verifying 5G orchestration, considering simultaneous access and admission of new requests to slices as well as virtual network function scheduling and routing. By combining modeling in user-friendly UML, with UPPAAL model checking and satisfiability-modulo-theories-based model finding, our framework supports both modeling and formal verification of service orchestration. We demonstrate our approach on a e-health case study showing how a user, with no knowledge of formal methods, can model a system in UML and verify that the application meets its requirements. © 2023, ComSIS Consortium. All rights reserved.

  • 6.
    Belli, Fevzi
    et al.
    University of Paderborn, Germany.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Panel Description: 40 Years of Software Engineering2008In: Proceedings 32nd Annual IEEE International Computer Software and Applications Conference, COMPSAC2008, 2008, p. 7-7Conference paper (Other academic)
    Abstract [en]

    In the fall of 1968, NATO hosted in Garmisch- Partenkirchen, close to Munich, a conference devoted to the problems of the computer industry that was having a great deal of trouble in producing large and complex programs. The term Software Engineering (SE) was not in general use at that time, its adoption for the title of this conference was deliberately provocative. As a result, the conference and its report have played a major role in gaining general acceptance of the term SE.

  • 7.
    Björnander, Stefan
    et al.
    CrossControl AB.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    A Formal Analysis Framework for AADL2011In: The Journal of Science and Technology, ISSN 0866-708X, Vol. 49, no 5Article in journal (Refereed)
    Abstract [en]

    As system failure of mission-critical embedded systems may result in serious consequences, the development process should include verification techniques already at the architectural design stage, in order to provide evidence that the architecture fulfils its requirements. The Architecture Analysis and Design Language (AADL) is a language designed for modeling embedded systems, and its Behavior Annex defines the behavior of the system. However, even though it is an internationally used industry standard, AADL still lacks a formal semantics and is not executable, which limits the possibility to perform formal verification. In this paper, we introduce a formal analysis framework for a subset of AADL and its Behavior Annex, which includes the following: a denotational semantics, its implementation in Standard ML, and a graphical Eclipse-based tool encapsulating the implementation. We also show how to perform model checking of AADL properties defined in the Computation Tree Logic (CTL).

  • 8.
    Björnander, Stefan
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    ABV: A Verifier for the Architecture Analysis and Description Language (AADL)2011In: 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2011, 2011, p. 355-360Conference paper (Refereed)
    Download full text (pdf)
    fulltext
  • 9.
    Björnander, Stefan
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    The Architecture Analysis and Design Language and the Behavior Annex: A Denotational Semantics2011Report (Other academic)
    Abstract [en]

    We present a denotational semantics for the Architecture Analysis and Design Language with Behavior Annex and the Computational Tree logic. We also present tool support as an OSATE plug-in as well as the Production Cell case study.

  • 10.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
    A Formal Approach for Flexible Modeling and Analysis of Transaction Timeliness and Isolation2016In: Proceedings of the 24th International Conference on Real-Time Networks and Systems, Brest, France, 2016Conference paper (Refereed)
    Abstract [en]

    Traditional Concurrency Control (CC) mechanisms ensure absence of undesired interference in transaction-based systems and enforce isolation. However, CC may introduce unpredictable delays that could lead to breached timeliness, which is unwanted for real-time transactions. To avoid deadline misses, some CC algorithms relax isolation in favor of timeliness, whereas others limit possible interleavings by leveraging real-time constraints and preserve isolation. Selecting an appropriate CC algorithm that can guarantee timeliness at an acceptable level of isolation thus becomes an essential concern for system designers. However, trading-off isolation for timeliness is not easy with existing analysis techniques in database and real-time communities. In this paper, we propose to use model checking of a timed automata model of the transaction system, in order to check the traded-off timeliness and isolation. Our solution provides modularization for the basic transactional constituents, which enables flexible modeling and composition of various candidate CC algorithms, and thus reduces the effort of selecting the appropriate CC algorithm.

  • 11.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
    Customized Real-Time Data Management for Automotive Systems: A Case Study2017In: IECON 2017 - 43RD ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2017, p. 8397-8404Conference paper (Refereed)
    Abstract [en]

    Real-time DataBase Management Systems (RTDBMS) have been considered as a promising means to manage data for data-centric automotive systems. During the design of an RTDBMS, one must carefully trade off data consistency and timeliness, in order to achieve an acceptable level of both properties. Previously, we have proposed a design process called DAGGERS to facilitate a systematic customization of transaction models and decision on the run-time mechanisms. In this paper, we evaluate the applicability of DAGGERS via an industrially relevant case study that aims to design the transaction management for an on-board diagnostic system, which should guarantee both timeliness and data consistency under concurrent access. To achieve this, we apply the pattern-based approach of DAGGERS to formalize the transactions, and derive the appropriate isolation level and concurrency control algorithm guided by model checking. We show by simulation that the implementation of our designed system satisfies the desired timeliness and derived isolation, and demonstrate that DAGGERS helps to customize desired real-time transaction management prior to implementation.

  • 12.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    DAGGTAX: A Taxonomy of Data Aggregation Processes2017Report (Other academic)
    Abstract [en]

    Data aggregation processes are essential constituents in many data management applications. Due to their complexity, designing data aggregation processes often demands considerable efforts. A study on the features of data aggregation processes will provide a comprehensive view for the designers and ease the design process. Existing works either propose application-specific aggregation solutions, or focus on particular aspects of aggregation processes such as aggregate functions, hence they do not offer a high-level, generic description. In this paper, we propose a taxonomy of data aggregation processes called DAGGTAX, which builds on the results of an extensive survey within various application domains. Our work focuses on the features of aggregation processes and their implications, especially on the temporal data consistency and the process timeliness. We present our taxonomy as a feature diagram, which is a visual notation with formal semantics. The taxonomy can then serve as the foundation of a design tool that enables designers to build an aggregation process by selecting and composing desired features. Based on the implications of the features, we formulate three design rules that eliminate infeasible feature combinations. We also provide a set of design heuristics that could help designers to decide the appropriate mechanisms for achieving the selected features. 

    Download full text (pdf)
    fulltext
  • 13.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    DAGGTAX: A taxonomy of data aggregation processes2017In: Lecture Notes in Computer Science, vol. 10563, Springer Verlag , 2017, p. 324-339Conference paper (Refereed)
    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. Due to the heterogeneity and real-time constraints in such systems, designing appropriate data aggregation processes often demands considerable effort. A study on the characteristics of data aggregation processes is then desirable, as it provides a comprehensive view of such processes, potentially facilitating their design, as well as the development of tool support to aid designers. In this paper, we propose a taxonomy called DAGGTAX, which is a feature diagram that models the common and variable characteristics of data aggregation processes, with a special focus on the real-time aspect. The taxonomy can serve as the foundation of a design tool, which we also introduce, enabling designers to build an aggregation process by selecting and composing desired features, and to reason about the feasibility of the design. We apply DAGGTAX on industrial case studies, showing that DAGGTAX not only strengthens the understanding, but also facilitates the model-driven design of data aggregation processes. © 2017, Springer International Publishing AG.

  • 14.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Data Aggregation Processes: A Survey, A Taxonomy, and Design Guidelines2019In: Computing, ISSN 0010-485X, E-ISSN 1436-5057, Vol. 101, no 10, p. 1397-1429Article in journal (Refereed)
    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.

  • 15.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems2018In: 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018, 2018, p. 355-374Conference 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.

  • 16.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Specification and Automated Verification of Atomic Concurrent Real-Time Transactions2019Manuscript (preprint) (Other academic)
  • 17.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Specification and Automated Verification of Atomic Concurrent Real-time Transactions2021In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, no 2, p. 557-589Article in journal (Refereed)
    Abstract [en]

    Many database management systems (DBMS) need to ensure atomicity and isolation of transactions for logical data consistency, as well as to guarantee temporal correctness of the executed transactions. Since the mechanisms for atomicity and isolation may lead to breaching temporal correctness, trade-offs between these properties are often required during the DBMS design. To be able to address this concern, we have previously proposed the pattern-based UPPCART framework, which models the transactions and the DBMS mechanisms as timed automata, and verifies the trade-offs with provable guarantee. However, the manual construction of UPPCART models can require considerable effort and is prone to errors. In this paper, we advance the formal analysis of atomic concurrent real-time transactions with tool-automated construction of UPPCART models. The latter are generated automatically from our previously proposed UTRAN specifications, which are high-level UML-based specifications familiar to designers. To achieve this, we first propose formal definitions for the modeling patterns in UPPCART, as well as for the pattern-based construction of DBMS models, respectively. Based on this, we establish a translational semantics from UTRAN specifications to UPPCART models, to provide the former with a formal semantics relying on timed automata, and develop a tool that implements the automated transformation. We also extend the expressiveness of UTRAN and UPPCART, to incorporate transaction sequences and their timing properties. We demonstrate the specification in UTRAN, automated transformation to UPPCART, and verification of the traded-off properties, via an industrial use case.

  • 18.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Specification and Formal Verification of Atomic Concurrent Real-Time Transactions2018In: 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 2018Conference 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.

  • 19.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Statistical Model Checking for Real-Time Database Management Systems: A Case Study2019In: The 24th IEEE Conference on Emerging Technologies and Factory Automation ETFA2019, 2019, p. 306-313Conference 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.

  • 20.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Towards the verification of temporal data consistency in Real-Time Data Management2016In: 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS, CPS Data 2016, 2016, article id Article number 7496422Conference paper (Refereed)
    Abstract [en]

    Many Cyber-Physical Systems (CPSs) require both timeliness of computation and temporal consistency of their data. Therefore, when using real-time databases in a real-time CPS application, the Real-Time Database Management Systems (RTDBMSs) must ensure both transaction timeliness and temporal data consistency. RTDBMSs prevent unwanted interferences of concurrent transactions via concurrency control, which in turn has a significant impact on the timeliness and temporal consistency of data. Therefore it is important to verify, already at early design stages that these properties are not breached by the concurrency control. However, most often such early on guarantees of properties under concurrency control are missing. In this paper we show how to verify transaction timeliness and temporal data consistency using model checking. We model the transaction work units, the data and the concurrency control mechanism as a network of timed automata, and specify the properties in TCTL. The properties are then checked exhaustively and automatically using the UPPAAL model checker. 

  • 21.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Trading-off Data Consistency for Timeliness in Real-Time Database Systems2015In: 27th Euromicro Conference on Real-Time Systems ECRTS'15, 2015, p. 13-16Conference paper (Refereed)
    Abstract [en]

    In order to guarantee transaction timeliness, Realtime Database Management Systems (RTDBMSs) often relax data consistency by relaxing the ACID transaction properties. Such relaxation varies depending on the application and thus different transaction management mechanisms have to be decided for developing a tailored RTDBMS. However, current RTDBMSs development does not include systematic verification of timeliness and desired ACID properties. Consequently, the implemented transaction management mechanisms may breach timeliness of transactions. In this paper, we propose a process called DAGGERS for developing a tailored RTDBMS that guarantees timeliness and desired data consistency for real-time systems by employing model-checking techniques during the process. Based on the characteristics of the desired data manipulations, transaction models are designed and then formally verified iteratively together with selected run-time mechanisms, in order to achieve the desired/necessary trade-offs between timeliness and data consistency. The outcome of DAGGERS is thus a tailored transaction management with guaranteed appropriate trade-offs, as well as the model-checking based worst-case execution times and blocking times of transactions under these mechanisms and assumptions of the hardware architecture.

  • 22.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Larsson, A.
    Ericsson AB, Stockholm, Sweden.
    Tool-supported design of data aggregation processes in cloud monitoring systems2019In: Journal of Ambient Intelligence and Humanized Computing, ISSN 1868-5137, E-ISSN 1868-5145, Vol. 10, no 7, p. 2519-2535Article in journal (Refereed)
    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.

  • 23.
    Cai, Simin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gallina, Barbara
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyström, Dag
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Larsson, Alf
    Ericsson AB, Stockholm, Sweden.
    Design of Cloud Monitoring Systems via DAGGTAX: A Case Study2017In: Procedia Computer Science, E-ISSN 1877-0509, Vol. 109, p. 424-431Article in journal (Refereed)
    Abstract [en]

    Efficient auto-scaling of cloud resources relies on the monitoring of the cloud, which involves multiple aggregation processes and large amounts of data with various and interdependent requirements. A systematic way of describing the data together with the possible aggregations is beneficial for designers to reason about the properties of these aspects as well as their implications on the design, thus improving quality and lowering development costs. In this paper, we propose to apply DAGGTAX, a feature-oriented taxonomy for organizing common and variable data and aggregation process properties, to the design of cloud monitoring systems. We demonstrate the effectiveness of DAGGTAX via a case study provided by industry, which aims to design a cloud monitoring system that serves auto-scaling for a video streaming system. We design the cloud monitoring system by selecting and composing DAGGTAX features, and reason about the feasibility of the selected features. The case study shows that the application of DAGGTAX can help designers to identify reusable features, analyze trade-offs between selected features, and derive crucial system parameters.

  • 24.
    Causevic, Adnan
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Distributed energy management case study: A formal approach to analyzing utility functions2014In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, p. 74-87Conference paper (Refereed)
    Abstract [en]

    The service-oriented paradigm has been established to enable quicker development of new applications from already existing services. Service negotiation is a key technique to provide a way of deciding and choosing the most suitable service, out of possibly many services delivering similar functionality but having different response times, resource usages, prices, etc. In this paper, we present a formal approach to the clients-providers negotiation of distributed energy management. The models are described in our recently introduced REMES HDCL language, with timed automata semantics that allows us to apply UPPAALbased tools for model-checking various scenarios of service negotiation. Our target is to compute ways of reaching the price- and reliability-optimal values of the utility function, at the end of the service negotiation.

  • 25.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Analyzing Resource-Usage Impact on Component-Based Systems Performance and Reliability2008In: 2008 International Conference on Computational Intelligence for Modelling Control & Automation, Los Alamitos, CA: IEEE Computer Society , 2008, p. 302-308Conference paper (Refereed)
    Abstract [en]

    An early prediction of resource utilization and its impacton system performance and reliability can reduce theoverall system cost, by allowing early correction of detectedproblems, or changes in development plans with minimizedoverhead. Nowadays, researchers are using both academicand commercial models to predict such attributes, by measuringthem at earliest stages of system development. Inthis paper, we give a short overview of existing predictionmodels for performance and reliability, targeting popularcomponent-based frameworks. Next, we describe our ownapproach for tackling such predictions, through an illustrationon a small example that deals with estimations of energyconsumption.

    Download full text (pdf)
    FULLTEXT02
  • 26.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Algorithmic Computation of Strongest Postconditions of Services as Priced Timed Automata2012Report (Other academic)
    Abstract [en]

    Service-Oriented Systems (SOS) have gained importance in different application domains thanks to their ability to enable reusable functionality provided via well-defined interfaces, and the increased opportunities to compose existing units, called services, into various configurations. Developing applications in such a setup, by reusing existing services, brings some concerns regarding the assurance of the expected Quality-of-Service (QoS), and correctness of the employed services. In this paper, we provide a formal mechanism of computing service guarantees, automatically. We assume service models annotated with pre- and postconditions, their semantics given as Priced Timed Automata (PTA), and the forward analysis method for checking the service correctness w.r.t. given requirements. Under these assumptions, we show how to compute the strongest postcondition of the corresponding automata algorithmically, with respect to the specified precondition. The approach is illustrated on a small example of a service modeled as Priced Timed Automaton (PTAn).

  • 27.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    An Analyzable Model of Automated Service Negotiation2013In: Proceedings - 2013 IEEE 7th International Symposium on Service-Oriented System Engineering, SOSE 2013, 2013, p. 125-136Conference paper (Refereed)
    Abstract [en]

    Negotiation is a key aspect of Service-Oriented Systems, which is rarely supported by formal models and tools for analysis. Often, service negotiation proceeds with timing, cost and resource constraints, under which the users and providers exchange information on their respective goals, until reaching a consensus. Consequently, a mathematically driven technique to analyze various ways to achieve such goals is beneficial. In this paper, we propose an analyzable negotiation model between service clients and providers, in our recently introduced language REMES and its corresponding textual service composition language HDCL. The model can be viewed as a negotiation interface for different negotiation strategies and protocols, which iterates until an agreement is reached. We show how to analyze the negotiation model against timing, cost and utility constraints, by transforming it into the Timed Automata formal framework. We illustrate our approach through an insurance scenario assuming a form of the Contract Net Protocol for web services.

  • 28.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Behavioral Modeling and Refinement of Services2009In: Prodceedings of 21st Nordic Workshop on Programming Theory, NWPT '09, 2009Conference paper (Refereed)
  • 29.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Checking Correctness of Services Modeled as Priced Timed Automata2012In: Lecture Notes in Computer Science, vol. 7610, issue part 2, Springer, 2012, p. 308-322Chapter in book (Refereed)
    Abstract [en]

    Service-Oriented Systems (SOS) have gained importance in different application domains thanks to their ability to enable reusable functionality provided via well-defined interfaces, and the increased opportunities to compose existing units, called services, into various configurations. Developing applications in such a setup, by reusing existing services, brings some concerns regarding the assurance of the expected Quality-of-Service (QoS), and correctness of the employed services. In this paper, we describe a formal mechanism of computing service guarantees, automatically. We assume service models annotated with pre- and postconditions, with their semantics given as Priced Timed Automata (PTA), and the forward analysis method for checking the service correctness w.r.t. given requirements. Under these assumptions, we show how to compute the strongest postcondition of the corresponding automata algorithmically, with respect to the specified precondition. The approach is illustrated on a small example of a service modeled as Priced Timed Automaton (PTAn).

  • 30.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Distributed Energy Management Case Study: A Formal Approach to Analyzing Utility Functions2013Report (Other academic)
    Abstract [en]

    The service-oriented paradigm has been established to enable quicker development of new applications from already existing services. Service negotiation is a key technique to provide a way of deciding and choosing the most suitable service, out of possibly many services delivering similar functionality but having different response times, resource usages, prices, etc. In this paper, we present a formal approach to the clients-providers negotiation of distributed energy management. The models are described in our recently introduced REMES HDCL language, with timed automata semantics that allows us to apply UPPAAL-based tools for model-checking various scenarios of service negotiation. Our target is to compute ways of reaching the price- and reliability-optimal values of the utility function, at the end of the service negotiation.

  • 31.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Formal reasoning of resource-aware services2010Report (Other academic)
    Abstract [en]

    Service-oriented systems have recently emerged as context-independent component-based systems. Unlike components, services can be created, invoked, composed, and destroyed at run-time. Consequently, all services should have a way of advertising their capabilities to the entities that will use them, and service-oriented modeling should cater for various kinds of service composition. In this paper, we show how services can be formally described by the resource-aware timed behavioral language REMES, which we extend with service-specific information, such as type, capacity, time-to-serve, etc., as well as boolean constraints on inputs, and output guarantees. Assuming a Hoare-triple model of service correctness, we show how to check it by using the strongest postcondition semantics. To provide means for connecting REMES services, we propose a hierarchical language for service composition, which allows for verifying the latter’s correctness. The approach is applied on an abstracted version of an intelligent shuttle system, for which we also compute resource-efficient behaviors, and energy-time trade-offs, by model-checking the system’s underlying Priced Timed Automata semantic representation.

  • 32.
    Causevic, Aida
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Modeling and Reasoning about Service Behaviors and their Compositions2010In: Lecture Notes in Computer Science, vol. 6416, Berlin: Springer , 2010, p. 82-96Chapter in book (Refereed)
    Abstract [en]

    Service-oriented systems have recently emerged as context-independent component-based systems. Unlike components, services can be created, invoked, composed, and destroyed at run-time. Consequently, all services need a way of advertising their capabilities to the entities that will use them, and serviceoriented modeling should cater for various kinds of service composition. In this paper, we show how services can be formally described by the resource-aware timed behavioral language REMES, which we extend with service-specific information, such as type, capacity, time-to-serve, etc., as well as boolean constraints on inputs, and output guarantees. Assuming a Hoare-triple model of service correctness, we show how to check it by using the strongest postcondition semantics. To provide means for connecting REMES services, we propose a hierarchical language for service composition, which allows for verifying the latter's correctness. The approach is applied on an abstracted version of an intelligent shuttle system.

  • 33.
    Cavalcanti, Ana
    et al.
    Univ York, York, N Yorkshire, England..
    Petrucci, Laure
    CNRS, LIPN, Paris, France.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems2018In: ERCIM News, ISSN 0926-4981, E-ISSN 1564-0094, no 112, p. 47-47Article in journal (Other academic)
    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.

  • 34.
    Dust, Lukas
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gu, Rong
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Ekström, Mikael
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mubeen, Saad
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pattern-Based Verification of ROS 2 Nodes Using UPPAAL2023In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Science and Business Media Deutschland GmbH , 2023, p. 57-75Conference paper (Refereed)
    Abstract [en]

    This paper proposes a pattern-based modeling and Uppaal-based verification of latencies and buffer overflow in distributed robotic systems that use ROS 2. We apply pattern-based modeling to simplify the construction of formal models for ROS 2 systems. Specifically, we propose Timed Automata templates for modeling callbacks in Uppaal, including all versions of the single-threaded executor in ROS 2. Furthermore, we demonstrate the differences in callback scheduling and potential errors in various versions of ROS 2 through experiments and model checking. Our formal models of ROS 2 systems are validated in experiments, as the behavior of ROS 2 presented in the experiments is also exposed by the execution traces of our formal models. Moreover, model checking can reveal potential errors that are missed in the experiments. The paper demonstrates the application of pattern-based modeling and verification in distributed robotic systems, showcasing its potential in ensuring system correctness and uncovering potential errors.

  • 35.
    Dust, Lukas
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Persson, Emil
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Ekström, Mikael
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mubeen, Saad
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Gu, Rong
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Experimental Evaluation of Callback Behavior in ROS 2 Executors2023In: IEEE Int. Conf. Emerging Technol. Factory Autom., ETFA, Institute of Electrical and Electronics Engineers Inc. , 2023Conference paper (Refereed)
    Abstract [en]

    Robot operating system 2 (ROS 2) is increasingly popular both in research and commercial robotic systems. ROS 2 is designed to allow real-time execution and data communication, enabling rapid prototyping and deployment of robotic systems. In order to predict and calculate execution times in ROS 2, one needs to analyze its internal scheduler, called executor. The executor has been updated in various distributions of ROS 2, which is shown to impact significantly the periodic execution invoked by the underlying operating system's timers, potentially causing unexpected latencies. To expose the mentioned impact due to executor differences, in this paper, we present an experimental evaluation of the execution behavior of ROS 2's schedulable entities, namely callbacks, among the existing versions of the executor. We visualize the differences of callback execution order via simulation, and we create design-level scenarios that impact the execution of periodically scheduled callbacks, negatively. Moreover, we show how such negative impact can be mitigated by using multi-threaded executors. Finally, we illustrate the observed behavior on a real-world centralized multi-agent robot system. Our work aims to raise awareness within the ROS 2 developer community, regarding possible problems of timer blocking, and propose a mitigation solution of the latter.

  • 36.
    Díaz, I. G.
    et al.
    Faculty of Social Sciences, University of Castilla-La Mancha, Spain.
    Lares, J. G. U.
    Division of Engineering and Exact Sciences, Anáhuac Mayab University, Mexico.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Special issue on Ambient Intelligence in the IoT: Convergence Trends and Challenges (AmIIoT)2022In: Journal of Ambient Intelligence and Humanized Computing, ISSN 1868-5137, E-ISSN 1868-5145Article in journal (Refereed)
  • 37.
    Enoiu, Eduard Paul
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Causevic, Aida
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    A Design Tool for Service-oriented Systems2013In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 295, p. 95-100Article in journal (Other academic)
    Abstract [en]

    In this paper we present a modeling and analysis tool for service-oriented systems. The tool enables graphical modeling of service-based systems, within the resource-aware timed behavioral language Remes, as well as a textual system description. We have developed a graphical environment where services can be composed as desired by the user, together with a textual service composition interface in which compositions can also be checked for correctness. We also provide automated traceability between the two design interfaces, which results in a tool that enhances the potential of system design by intuitive service manipulation. The paper presents the design principles, infrastructure, and the user interface of our tool.

    Download full text (pdf)
    FESCA2012 - A Design Tool for Service-oriented Systems
  • 38.
    Enoiu, Eduard Paul
    et al.
    Mälardalen University.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Paul, Pettersson
    Mälardalen University, School of Innovation, Design and Engineering.
    ViTAL : A Verification Tool for EAST-ADL Models using UPPAAL PORT2012In: Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, Paris, France, 2012, p. 328-337Conference paper (Refereed)
    Abstract [en]

    A system’s architecture influence on the functions and other properties of embedded systems makes its high level analysis and verification very desirable. EAST-ADL is an architecture description language dedicated to automotive embedded system design with focus on structural and functional modeling. The behavioral description is not integrated within the execution semantics, which makes it harder to transform, analyze, and verify EAST-ADL models. Model-based techniques help address this issue by enabling automated transformation between different design models, and providing means for simulation and verification. We present a verification tool, called ViTAL, which provides the possibility to express the functional EAST-ADL behavior as timed automata models, which have precise semantics and can be formally verified. The ViTAL tool enables the transformation of EAST-ADL functional models to the UPPAAL PORT tool for model checking. This method improves the verification of functional and timing requirements in EAST-ADL, and makes it possible to identify dependencies and potential conflicts between different vehicle functions before the actual AUTOSAR implementation.

    Download full text (pdf)
    fulltext
  • 39.
    Enoiu, Eduard Paul
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Towards the Analysis and Verification of EAST-ADL Models using UPPAAL PORT2012Report (Other academic)
    Abstract [en]

    A system’s architecture influence on the functions and other properties of embedded systems makes its high level analysis and verification very desirable. EAST-ADL is an architecture description language dedicated to automotive embedded system design with focus on structural and functional modeling. The behavioral description is not integrated within the execution semantics, which makes it harder to transform, analyze, and verify EAST-ADL models. Model-based techniques help address this issue by enabling automated transformation between different design models, and providing means for simulation and verification. We present a verification tool, called ViTAL, which provides the possibility to express the functional EAST-ADL behavior as timed automata models, which have precise semantics and can be formally verified. The ViTAL tool enables the transformation of EAST-ADL functional models to the UPPAAL PORT tool for model checking. This method improves the verification of functional and timing requirements in EAST-ADL, and makes it possible to identify dependencies and potential conflicts between different vehicle functions before the actual AUTOSAR implementation.

    Download full text (pdf)
    fulltext
  • 40.
    Enoiu, Eduard Paul
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Model Testing of Complex Embedded Systems using EAST-ADL and Energy-Aware Mutations2020In: Designs, ISSN 2411-9660, Vol. 4, no 1, p. 1-18, article id 5Article in journal (Refereed)
    Abstract [en]

    Nowadays, embedded systems are increasingly complex, meaning that traditional testing methods are costly to use and infeasible to directly apply due to the complex interactions between hardware and software. Modern embedded systems are also demanded to function based on low-energy computing. Hence, testing the energy usage is increasingly important. Artifacts produced during the development of embedded systems, such as architectural descriptions, are beneficial abstractions of the system’s complex structure and behavior. Electronic Architecture and Software Tools Architecture Description Language (EAST-ADL) is one such example of a domain-specific architectural language targeting the automotive industry. In this paper, we propose a method for testing design models using EAST-ADL architecture mutations. We show how fault-based testing can be used to generate, execute and select tests using energy-aware mutants-- syntactic changes in the architectural description, used to mimic naturally occurring energy faults. Our goal is to improve testing of complex embedded systems by moving the testing bulk from the actual systems to models of their behaviors and non-functional requirements. We combine statistical model-checking, increasingly used in quality assurance of embedded systems, with EAST-ADL architectural models and mutation testing to drive the search for faults. We show the results of applying this method on an industrial-sized system developed by Volvo GTT. The results indicate that model testing of EAST-ADL architectural models can reduce testing complexity by bringing early and cost-effective automation.

  • 41.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Jagerfield, Trevor
    Mälardalen University.
    Nyberg, Mattias
    Scania, Södertälje, Sweden.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain2016In: PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2, 2016, Vol. 2, p. 167-173, article id 7552198Conference paper (Refereed)
    Abstract [en]

    The lack of formal system specifications is a major obstacle to the widespread adoption of formal verification techniques in industrial settings. Specification patterns represent a promising approach that can fill this gap by enabling non-expert practitioners to write formal specifications based on reusing solutions to commonly occurring problems. Despite the fact that the specification patterns have been proven suitable for specification of industrial systems, there is no engineer-friendly tool support adequate for industrial adoption. In this paper, we present a tool called SESAMM Specifier in which we integrate a subset of the specification patterns for formal requirements specification, called SPS, into an existing industrial tool-chain. The tool provides the necessary means for the formal specification of system requirements and the later validation of the formally expressed behavior.

  • 42.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mahmud, Nesredin
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Ljungkrantz, Oscar
    Volvo Group Trucks Technology, Gothenburg, Sweden.
    Lönn, Henrik
    Volvo Group Trucks Technology, Gothenburg, Sweden.
    Analyzing Industrial Simulink Models by Statistical Model Checking2017Report (Other academic)
    Abstract [en]

    The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose a pattern-based, execution-order preserving automatic transformation of Simulink atomic and composite blocks into stochastic timed automata that can then be analyzed formally with UPPAAL Statistical Model Checker (UPPPAAL SMC). Our method is supported by the tool SIMPPAAL, which we also introduce and apply on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.

  • 43.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mahmud, Nesredin
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Ljungkrantz, Oscar
    Volvo Group Trucks TechnologyGothenburgSweden.
    Lönn, Henrik
    Volvo Group Trucks TechnologyGothenburgSweden.
    Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems2016In: FM 2016: Formal Methods, 2016, p. 748-756Conference paper (Refereed)
    Abstract [en]

    The advanced technology used for developing modern automotive systems increases their complexity, making their correctness assurance very tedious. To enable analysis, but also enhance understanding and communication, by simulation, engineers use MATLAB/Simulink modeling during system development. In this paper, we provide further analysis means to industrial Simulink models by proposing a pattern-based, execution-order preserving transformation of Simulink blocks into the input language of UPPAAL Statistical Model checker, that is, timed (hybrid) automata with stochastic semantics. The approach leads to being able to analyze complex Simulink models of automotive systems, and we report our experience with two vehicular systems, the Brake-by-Wire and the Adjustable Speed Limiter.

  • 44.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyberg, Mattias
    Scania AB CV, Södertälje, Sweden.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Automated SMT-based Consistency Checking of Industrial Critical Requirements2017In: ACM SIGAPP Applied Computing Review, ISSN 1559-6915, E-ISSN 1931-0161, Vol. 17, no 4, p. 15-28Article in journal (Refereed)
    Abstract [en]

    With the ever-increasing size, complexity and intricacy of system requirements specifications, it becomes difficult to ensure their correctness with respect to certain criteria such as consistency. Automated formal techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. Sometimes such techniques incur a high modeling cost or analysis time, or are not applicable. To address such problems, in this paper we propose an automated consistency analysis technique of requirements that are formalized based on patterns, and checked using state-of-the-art Satisfiability Modulo Theories solvers. Our method assumes several transformation steps, from textual requirements to formal logic, and next into the format suited for the SMT tool. To automate such steps, we propose a tool, called PROPAS, that does not require any user intervention during the transformation and analysis phases, thus making the consistency analysis usable by non-expert practitioners. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive system called the Fuel Level Display.

  • 45.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyberg, Mattias
    Scania, Sweden.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    SMT-based Consistency Analysis of Industrial Systems Requirements2017In: Proceedings of the ACM Symposium on Applied Computing, Volume Part F12800, 2017, no 5, p. 1272-1279Conference paper (Refereed)
    Abstract [en]

    As the complexity of industrial systems increases, it becomes dificult to ensure the correctness of system requirements specifications with respect to certain criteria such as consistency. Automated techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. However, such approaches can some-times be costly in terms of modeling and analysis time or not applicable for certain types of properties. In this paper, we present a complementary method that relies on pattern-based formalization of requirements and automated consistency checking using the state-of-the-art SMT tool Z3. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive subsystem called the Fuel Level Display. 

  • 46.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Bounded Invariance Checking of Simulink Models2019In: Proceedings of the ACM Symposium on Applied Computing, 2019, Vol. Part F147772, p. 2168-2177Conference 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. 

  • 47.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience2018In: Electronic Communications of the EASST, E-ISSN 1863-2122, Vol. 75, p. 1-20Article in journal (Refereed)
    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.

  • 48.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners2019In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019, 2019, p. 92-103Conference 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. 

  • 49.
    Foughali, M.
    et al.
    LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France.
    Ingrand, F.
    LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Statistical Model Checking of Complex Robotic Systems2019In: Model Checking Software, SPIN 2019, Springer , 2019, p. 114-134Conference 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.

  • 50.
    Gu, Rong
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Baranov, Eduard
    UCLouvain, Belgium.
    Ameri, Afshin
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Enoiu, Eduard Paul
    Curuklu, Baran
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Legay, Alex
    UCLouvain, Belgium.
    Lundqvist, Kristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road ConditionsManuscript (preprint) (Other academic)
    Abstract [en]

    Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy the given requirements. In this article, we propose a mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements,  a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it on a special case of the industrial case study.

123 1 - 50 of 144
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf