| 1. |
- Mahmud, Nesredin, et al.
(författare)
-
Power-aware Allocation of Fault-tolerant Multi-rate AUTOSAR Applications
- 2018
-
Ingår i: 25th Asia-Pacific Software Engineering Conference APSEC'18. - : Institute of Electrical and Electronics Engineers (IEEE). - 9781728119700
-
Konferensbidrag (refereegranskat)abstract
- This paper proposes an Integer Linear Programming optimization approach for the allocation of fault-tolerant embedded software applications that are developed using the AUTOSAR standard. The allocation takes into account the timing and reliability requirements of the multi-rate cause-effect chains in these applications and the heterogeneity of their execution platforms. The optimization objective is to minimize the total power consumption of the these applications that are distributed over more than one computing unit. The proposed approach is evaluated using a range of different software applications from the automotive domain, which are generated using the real-world automotive benchmark. The evaluation results indicate that the proposed allocation approach is effective and scalable while meeting the timing, reliability and power requirements in small- and medium-sized automotive software applications.
|
|
| 2. |
- Awada, Imad Alex, et al.
(författare)
-
An end- user perspective on the CAMI Ambient and Assisted Living Project
- 2018
-
Ingår i: INTED2018 Proceedings. - : IATED. - 9788469794807 ; , s. 6776-6785
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 3. |
- Backeman, Peter, et al.
(författare)
-
Supporting 5G Service Orchestration with Formal Verification
- 2023
-
Ingår i: Computer Science and Information Systems. - : ComSIS Consortium. - 1820-0214. ; 29:1, s. 329-357
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 4. |
- Belli, Fevzi, et al.
(författare)
-
Panel Description : 40 Years of Software Engineering
- 2008
-
Ingår i: Proceedings 32nd Annual IEEE International Computer Software and Applications Conference, COMPSAC2008. ; , s. 7-7
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
| 5. |
- Cai, Simin, et al.
(författare)
-
Customized Real-Time Data Management for Automotive Systems : A Case Study
- 2017
-
Ingår i: IECON 2017 - 43RD ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY. - 9781538611272 ; , s. 8397-8404
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 6. |
- Cai, Simin, et al.
(författare)
-
DAGGTAX : A Taxonomy of Data Aggregation Processes
- 2017
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
| 7. |
- Cai, Simin, et al.
(författare)
-
Data Aggregation Processes : A Survey, A Taxonomy, and Design Guidelines
- 2019
-
Ingår i: Computing. - : Springer Science and Business Media LLC. - 0010-485X .- 1436-5057. ; 101:10, s. 1397-1429
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 8. |
- Cai, Simin, et al.
(författare)
-
Design of Cloud Monitoring Systems via DAGGTAX : A Case Study
- 2017
-
Ingår i: Procedia Computer Science. - : Elsevier BV. - 1877-0509. ; 109, s. 424-431
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 9. |
- Cai, Simin, et al.
(författare)
-
Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems
- 2018
-
Ingår i: 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018. - Cham : Springer International Publishing. - 9783030034245 ; , s. 355-374
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 10. |
- Cai, Simin, et al.
(författare)
-
Specification and Automated Verification of Atomic Concurrent Real-time Transactions
- 2021
-
Ingår i: Software and Systems Modeling. - Germany : Springer Science and Business Media LLC. - 1619-1366 .- 1619-1374. ; :2, s. 557-589
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
