| 11. |
- Bakhshi, Zeinab, 1986-, et al.
(författare)
-
Analyzing the performance of persistent storage for fault-tolerant stateful fog applications
- 2023
-
Ingår i: Journal of systems architecture. - 1383-7621 .- 1873-6165. ; 144
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we analyze the scalability and performance of a persistent, fault-tolerant storage approach that provides data availability and consistency in a distributed container-based architecture with intended use in industrial control applications. We use simulation to evaluate the performance of this storage system in terms of scalability and failures. As the industrial applications considered have timing constraints, the simulation results show that for certain failure patterns, it is possible to determine whether the storage solution can meet critical deadlines. The presented approach is applicable for evaluating timing constraints also of other container-based critical applications that require persistent storage.
|
|
| 12. |
- Bakhshi, Zeinab, 1986-
(författare)
-
Lightweight Persistent Storage for Industrial Applications
- 2023
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Clouds are large computer centers that offer remote access to computing and storage resources, making them popular for business and web applications. They are now being considered for use in safety-critical applications such as factories, but lack sufficient time predictability, which makes it challenging to use them in these time-sensitive applications. To overcome this limitation, an intermediate layer, the fog layer, is introduced to provide computational resources closer to the network edge. However, this new computing paradigm faces its own challenges in resource management, scalability, and reliability due to resource constrained nodes. Lightweight virtualization technologies like containerization can solve the performance-reliability dichotomy in fog computing and provide built-in fault tolerance mechanisms. By studying a robotic use-case, we realized the critical importance of persistent data storage for stateful applications, such as many control applications. However, container-based solutions lack fault-tolerant persistent storage. In this thesis, we identify new challenges associated with leveraging container-based architectures, particularly the importance of persistent storage for stateful applications. We investigate the design possibilities for persistent fault-tolerant storage and propose a solution adapted to container-based fog architectures and tailored for stateful applications. The solution provides scalability, auto recovery, and re-integration after failures at application and node levels. Key elements are a replicated data structure and a storage container, using a consensus protocol for distributed data consistency and fault tolerance in case of node failures. The fault tolerance and consistency of the solution are modeled and verified, and its timing requirements evaluated. We use simulation to evaluate the timing performance of our solution in larger set-ups. The results of our study show that although adding a consistency protocol introduces a timing overhead, the solution still meets timing requirements for the studied use-case even in presence of a set of relevant faults. By leveraging a four-dimensional approach, we also conduct a comparative analysis of our solution with other approaches from various perspectives, indicating that our solution can be applied in a broader context than initially intended.
|
|
| 13. |
- Bakhshi, Zeinab, 1986-, et al.
(författare)
-
Storage placement in continuum computing for a robotic application
-
Annan publikation (övrigt vetenskapligt/konstnärligt)abstract
- This paper analyzes the timing performance of a persistent storage designed for distributed containerbased architectures in industrial control applications. The storage ensures data availability andconsistency while accommodating faults. The analysis considers four aspects: 1. placement strategy,2. design options, 3. data size, and 4. evaluation under faulty conditions. Experimental results considering the timing constraints in industrial applications indicate that the storage solution can meet criticaldeadlines, particularly under specific failure patterns. Moreover, this evaluation method is applicablefor assessing other container-based critical applications with timing constraints that require persistentstorage. Further comparison results reveal that, while the method may underperform current centralized solutions under fault-free conditions, it outperforms the centralized solutions in failure scenarios
|
|
| 14. |
- Ballesteros, A., et al.
(författare)
-
Achieving elementary cycle synchronization between masters in the flexible time-triggered replicated star for ethernet
- 2014
-
Ingår i: 19th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2014. - 9781479948468 ; , s. Article number 7005335-
-
Konferensbidrag (refereegranskat)abstract
- For a distributed embedded system (DES) to operate continuously in a dynamic environment, it must be flexible and highly reliable. This applies in particular to its communication subsystem. The Flexible Time-Triggered Replicated Star for Ethernet (FTTRS) aims at providing such a subsystem by means of a highly-reliable switched-Ethernet architecture based on the Flexible Time-Triggered paradigm (FTT), a master/slave communication paradigm where the master periodically polls the slaves using so-called trigger messages (TMs). In particular, FTTRS interconnects nodes by redundant communication paths provided by two switches, each embedding an FTT master that manages the communication. This allows FTTRS to tolerate the failure of one switch without interrupting the communication as long as the masters are replica determinate, i.e., provide identical service to the slaves. The master replica determinism entails the masters broadcasting their TMs in a lockstep fashion: when one master broadcasts a TM, the other should do the same quasi-simultaneously. In this paper we present a solution inspired by the Precision Time Protocol (PTP) for achieving this lockstep transmission and preliminary results showing the precision with which we can synchronize the masters on a software prototype.
|
|
| 15. |
- Filipovikj, Predrag, et al.
(författare)
-
2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings
- 2014
-
Ingår i: 2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings. - 9781479930333 ; , s. 444-450
-
Konferensbidrag (refereegranskat)abstract
- The importance of using formal methods and techniques for verification of requirements in the automotive industry has been greatly emphasized with the introduction of the new ISO26262 standard for road vehicles functional safety. The lack of support for formal modeling of requirements still represents an obstacle for the adoption of the formal methods in industry. This paper presents a case study that has been conducted in order to evaluate the difficulties inherent to the process of transforming the system requirements from their traditional written form into semi-formal notation. The case study focuses on a set of non-structured functional requirements for the Electrical and Electronic (E/E) systems inside heavy road vehicles, written in natural language, and reassesses the applicability of the extended Specification Pattern System (SPS) represented in a restricted English grammar. Correlating this experience with former studies, we observe that, as previously claimed, the concept of patterns is likely to be generally applicable for the automotive domain. Additionally, we have identified some potential difficulties in the transformation process, which were not reported by the previous studies and will be used as a basis for further research.
|
|
| 16. |
- Filipovikj, Predrag, et al.
(författare)
-
Analyzing Industrial Simulink Models by Statistical Model Checking
- 2017
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
| 17. |
- Filipovikj, Predrag, et al.
(författare)
-
Automated SMT-based Consistency Checking of Industrial Critical Requirements
- 2017
-
Ingår i: ACM SIGAPP Applied Computing Review. - United States : ACM. - 1559-6915 .- 1931-0161. ; 17:4, s. 15-28
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 18. |
- Filipovikj, Predrag, et al.
(författare)
-
Bounded Invariance Checking of Simulink Models
- 2019
-
Ingår i: Proceedings of the ACM Symposium on Applied Computing. - New York, NY, USA : ACM. ; , s. 2168-2177
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 19. |
- Filipovikj, Predrag, et al.
(författare)
-
Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain
- 2016
-
Ingår i: PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2<em></em>. - 9781467388450 ; , s. 167-173
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 20. |
- Filipovikj, Predrag, et al.
(författare)
-
Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements : Application and Experience
- 2018
-
Ingår i: Electronic Communications of the EASST. - Germany. - 1863-2122. ; 75, s. 1-20
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
