| 11. |
- Mahmud, Nesredin
(författare)
-
Design of Assured and Efficient Safety-critical Systems
- 2019
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Safety-critical systems need to be analyzed rigorously to remove software/specifications errors, that is, their requirements specifications should be unambiguous, comprehensible and consistent, and the software design should conform to the specifications, hence avoiding undesirable system failures. Currently, there is a lack of effective and scalable methods to specify and analyze requirements, and formally analyze the behavioral models of embedded systems. Most embedded systems requirements are expressed in natural language, which is flexible and intuitive but frequently ambiguous and incomprehensible. Besides natural language, template-based requirements specification methods are used frequently to specify requirements (esp. in safety-critical applications). Although the latter reduce ambiguity and improve the comprehensibility of the specifications, they are usually rigid due to the constrained syntax of the templates, and template selection is challenging. Industrial systems are frequently developed by using modeling and simulation environments such as Simulink, which is also used to generate code automatically for various hardware platforms. Therefore, it is essential to be able to formally analyze Simulink models, to get insight into the behavior of the embedded system, and also prevent potential errors from propagating into the implementation. Analyzing the timing behavior of safety-critical software that is refined by multi-rate periodic tasks with data age constraints across the end-to-end software functionality is not trivial. This is due to the undersampling and oversampling effects caused by the data propagation from higher to lower rates and vice versa, respectively. Furthermore, when such systems are deployed on a distributed architecture, e.g., electrical/electronic vehicular system, besides assuring the timeliness, the reliability of the distributed software should be maximized to counter the higher risk of failures in the distributed computing setting, hence improving the overall predictability of the safety-critical system. However, designing for reliability usually requires additional critical system resources such as energy. Hence, to accommodate the growing complexity of software functionality, the design of the safety-critical systems should consider the efficient use of critical system resources such as the power source, while meeting the timing and reliability requirements.To address the above needs, in this thesis, we propose formal-methods-based approaches and optimization techniques to assure improved quality of requirements specifications and software designs, and to efficiently map software functionality to hardware. The contributions of the thesis are: (i) ReSA - a domain-specific requirements specification language tailored to embedded systems, based on constrained natural language; (ii) a formal approach to check consistency of ReSA specifications via Boolean satisfiability problem (SAT) and ontology; (iii) a framework based on statistical model checking to analyze Simulink models via automated transformation into networks of stochastic timed automata; and (iv) a resource-efficient allocation of fault-tolerant software with end-to-end timing and reliability constraints via integer linear programming and hybrid particle-swarm optimization. Our proposed solutions are validated and evaluated on automotive use cases such as the Adjustable Speed Limiter (ASL) and the Brake-by-Wire (BBW) systems from Volvo Group Trucks Technology (VGTT), and on an Engine Management (EM) system benchmark from Bosch.
|
|
| 12. |
- Mahmud, Nesredin
(författare)
-
Ontology-based Analysis and Scalable Model Checking of Embedded Systems Models
- 2017
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Currently, there is lack of effective and scalable methods to specify and ana-lyze requirements specifications, and verify the behavioral models of embed-ded systems. Most embedded systems requirements are expressed in naturallanguage which is flexible and intuitive but frequently ambiguous, vague andincomprehensive. Besides to natural language, template-based requirementsspecification methods are used to specify requirements specifications (esp. insafety-critical applications), which reduce ambiguity and improves the com-prehensibility of the specifications. However, the template-based method areusually rigid due to the fixed structures of the templates. They also lack meta-models for extensibility, and template selection is challenging.In this thesis, we proposed a domain specific language for embedded sys-tems, called ReSA, which is constrained natural language but flexible enoughto allow engineers to use different constructs to specify requirements. Thelanguage has formal semantics in proportional logic and description logic thatenables non-trivial and rigorous analysis of requirements specification, e.g.,consistency checking, completeness of specifications, etc.Moreover, we propose a scalable formal verification of Simulink models,whichisusedtodescribethebehaviorofsystemsthroughcommunicatingfunc-tional blocks. In industry, Simulink is the de facto modeling and analysis en-vironment of embedded systems. It is also used to generate code automati-cally from special Simulink models for various hardware platforms. However,Simulink lacks formal approach to verify large and hybrid Simulink models.Therefore, we also propose a formal verification of Simulink models, repre-sented as stochastic timed automata, using statistical model checking, whichhas proven to scale for industrial applications.We validate our approaches on industrial use cases from the automotiveindustry. These includes Adjustable Speed Limiter (ASL) and Brake-By-Wire(BBW) systems from Volvo Group Trucks Technology, both safety-critical.
|
|
| 13. |
- 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.
|
|
| 14. |
- Pozo, Francisco, et al.
(författare)
-
A decomposition approach for SMT-based schedule synthesis for time-triggered networks
- 2015
-
Ingår i: 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA). - 9781467379298 ; , s. Article number 7301436-
-
Konferensbidrag (refereegranskat)abstract
- Real-time networks have tight communication latency and minimal jitter requirements. One way to ensure these requirements is the implementation of a static schedule, which defines the transmission points in time of time-triggered frames. Synthesizing such static schedules is known to be an NP-complete problem where the complexity is driven by the large number of constraints imposed by the network. Satisfiabily Modulo Theories (SMT) have been proven powerful tools to synthesize schedules of medium-to-large industrial networks. However, the schedules of new extremely large networks, such as integrated multi-machine factory networks, are defined by an extremely large number of constraints exceeding the capabilities of being synthesized by the tool alone. This paper presents a decomposition approach that will allow us to improve to synthesize schedules with up to two orders of magnitude in terms of the number of constraints that can be handled. We also present an implementation of a dependency tree on top of the decomposition approach to address application-imposed constraints between frames.
|
|
| 15. |
- Pozo, Francisco, et al.
(författare)
-
Period-Aware Segmented Synthesis of Schedules for Multi-Hop Time-Triggered Networks
- 2016
-
Ingår i: 22nd IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2016). - : IEEE. ; , s. 170-175
-
Konferensbidrag (refereegranskat)abstract
- Time-triggered offline scheduling is a cost-efficien way to guarantee low communication end-to-end latency and minimal jitter for communication networks in real-time systems. The schedule is generated pre-runtime and indicates the transmission times of time-triggered frames such that contention is prevented. The synthesis of such offline schedules is a bin-packing problem, known to be NP-complete, with complexity driven by the constraints on frame transmissions, and the number of frames in the schedule. Satisfiability Modulo Theories combined with segmented approaches have been successfully used for synthesizing schedules of large networks. However, such synthesis did not take into account frames periods that are much shorter than the time to execute the schedule cycle. This paper presents a periodaware segmented approach that takes into account the frame periods in order to allocate various instances of a frame within a single cycle. We describe three different synthesis strategies and evaluate them with different synthetic experiments. The results show better performance for one of the strategies, which can synthesize schedules of large networks with high communication loads in less than one hour. We also report how the synthesis time and the schedule quality can change with different parameter configurations.
|
|
| 16. |
- Pozo, Francisco, et al.
(författare)
-
SMT-based synthesis of TTEthernet schedules : A performance study
- 2015
-
Ingår i: 2015 10th IEEE International Symposium on Industrial Embedded Systems, SIES 2015 - Proceedings. - 9781467377119 ; , s. 162-165
-
Konferensbidrag (refereegranskat)abstract
- Time-triggered networks, like TTEthernet, require adoption of a predefined schedule to guarantee low communication latency and minimal jitter. The synthesis of such schedules is a problem known to be NP-complete. In the past, specialized solvers have been used for synthesizing time-triggered schedules, but more recently general-purpose tools like Satisfiability Modulo Theories (SMT) solvers have reported synthesis of large network schedules in reasonable time for industrial purposes. An interesting characteristic of any general-purpose tool is that its configuration parameters can be tuned in order to fit specific problems and achieve increased performance. This paper presents a study identifying and assessing which SMT solver parameters have the highest impact on the performance when synthesizing schedules for time-triggered networks. The results show that with appropriate values of certain parameters, the time can be reduced significantly, up to 75% in the best cases compared to previous work. © 2015 IEEE.
|
|
| 17. |
- Pozo, Francisco
(författare)
-
Synthesis of Extremely Large Time-Triggered Network Schedules
- 2017
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Many embedded systems with real-time requirements demand minimal jitter and low communication end-to-end latency for its communication networks. The time-triggered paradigm, adopted by many real-time protocols, was designed to cope with these demands. A cost-efficient way to implement this paradigm is to synthesize a static schedule that indicates the transmission times of all the time-triggered frames such that all requirements are met. Synthesizing this schedule can be seen as a bin-packing problem, known to be NPcomplete, with complexity driven by the number of frames. In the last years, requirements on the amount of data being transmitted and the scalability of the network have increased. A solution was proposed, adapting real-time switched Ethernet to benefit from its high bandwidth. However, it added more complexity in computing the schedule, since every frame is distributed over multiple links. Tools like Satisfiability Modulo Theory solvers were able to cope with the added complexity and synthesize schedules of industrial size networks. Despite the success of such tools, applications are appearing requiring embedded systems with even more complex networks. In the future, real-time embedded systems, such as large factory automation or smart cities, will need extremely large hybrid networks, combining wired and wireless communication, with schedules that cannot be synthesized with current tools in a reasonable amount of time. With this in mind, the first thesis goal is to identify the performance limits of Satisfiability Modulo Theory solvers in schedule synthesis. Given these limitations, the next step is to define and develop a divide and conquer approach for decomposing the entire scheduling problem in smaller and easy solvable subproblems. However, there are constraints that relate frames from different subproblems. These constraints need to be treated differently and taken into account at the start of every subproblem. The third thesis goal is to develop an approach that is able to synthesize schedules when different frame constraints related to different subproblems are inter-dependent. Last, is to define the requirements that the integration of wireless communication in hybrid networks will bring to the schedule synthesis and how to cope with the increased complexity. We demonstrate the viability of our approaches by means of evaluations, showing that our method is capable to synthesize schedules of hundred of thousands of frames in less than 5 hours.
|
|
| 18. |
- Pozo Pérez, Francisco Manuel
(författare)
-
Methods for Efficient and Adaptive Scheduling of Next-Generation Time-Triggered Networks
- 2019
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Real-time networks play a fundamental role in embedded systems. To meet timing requirements, provide low jitter and bounded latency in such networks the time-triggered communication paradigm is frequently applied in such networks. In this paradigm, a schedule specifying the transmission times of all the traffic is synthesized a priori. Given the steady increase in size and complexity of embedded systems, coupled with the addition of wireless communication, a new time-triggered network model of larger and mixed wired-wireless network isdeveloping. Developing such next-generation networks entails significant research challenges, especially concerning scalability, i.e., allowing generation of schedules of the very large next-generation networks in a reasonable time. A second challenge concerns a well-known limitation of the time-triggered paradigm: its lack of flexibility. Large networks exacerbate this problem, as the number of changes during network operation increases with the number of components, which renders static scheduling approaches unsuitable.In this thesis, we first propose a remedy to the scalability challenge that the synthesis of next-generation network schedules introduces. We propose a family of divide-and-conquer approaches that segment the entire scheduling problem into small enough subproblems that can be effectively and efficiently solved by state-of-the-art schedulers. Second, we investigate how adaptive behaviours can be introduced into the time-triggered paradigm with the implementation of a Self-Healing Protocol. This protocol addresses the flexibility challenge by only updating a small segment of the schedule in response to changes during runtime. This provides a significant advantage compared to current approaches that fully reschedule the network. In the course of our research, we found that our protocol become more effective when the slack in the original schedule is evenly distributed during the schedule synthesis. As a consequence, we also propose a new scheduling approach that maximizes the distances between frames, increasing the success rate of our protocol.The divide-and-conquer approaches developed in this thesis were able to synthesize schedules of two orders of magnitude more traffic and one order of magnitude more nodes in less than four hours. Moreover, when applied to current industrial size networks, they reduced the synthesis time from half an hour to less than one minute compared with state-of-the-art schedulers. The Self-Healing Protocol opened a path towards adaptive time-triggered being able to heal schedules online after link and switch failures in less than ten milliseconds.
|
|
| 19. |
- Pozo Pérez, Francisco Manuel, et al.
(författare)
-
Methods for large-scale time-triggered network scheduling
- 2019
-
Ingår i: Electronics. - : MDPI AG. - 2079-9292. ; 8:7
-
Tidskriftsartikel (refereegranskat)abstract
- Future cyber–physical systems may extend over broad geographical areas, like cities or regions, thus, requiring the deployment of large real-time networks. A strategy to guarantee predictable communication over such networks is to synthesize an offline time-triggered communication schedule. However, this synthesis problem is computationally hard (NP-complete), and existing approaches do not scale satisfactorily to the required network sizes. This article presents a segmented offline synthesis method which substantially reduces this limitation, being able to generate time-triggered schedules for large hybrid (wired and wireless) networks. We also present a series of algorithms and optimizations that increase the performance and compactness of the obtained schedules while solving some of the problems inherent to segmented approaches. We evaluate our approach on a set of realistic large-size multi-hop networks, significantly larger than those considered in the existing literature. The results show that our segmentation reduces the synthesis time by up to two orders of magnitude.
|
|
| 20. |
- Pozo Pérez, Francisco Manuel, et al.
(författare)
-
Schedule reparability : Enhancing time-triggered network recovery upon link failures
- 2018
-
Ingår i: Proceedings - 2018 IEEE 24th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2018. - : Institute of Electrical and Electronics Engineers Inc.. - 9781538677599 ; , s. 147-156
-
Konferensbidrag (refereegranskat)abstract
- The time-triggered communication paradigm has been shown to satisfy temporal isolation while providing end to end delay guarantees through the synthesis of an offline schedule. However, this paradigm has severe flexibility limitations as any unpredicted change not anticipated by the schedule, such as a component failure, might result in a loss of frames. A typical solution is to use redundancy or replace and update the schedule offline anew. With the ever increase in size of networks and the need to reduce costs, supplementary solutions that enhance the reliability of such networks are also desired. In this paper, we introduce a repair algorithm capable of reacting to unpredicted link failures. The algorithm quickly modifies the schedule such that all frames are transmitted again within their timing guarantees. We found that the success of our algorithm increases significantly with the existence of empty slots spread over the schedule, an opposite approach compared to packing frames, commonly used in the literature. We propose a new ILP formulation that includes a maximization of frame and link intermissions to stretch empty slots over the schedule. Our results show that we can repair with 90% success rate within milliseconds to a valid schedule compared to a few minutes needed to re-schedule the whole network.
|
|
