mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Rodriguez-Navas, GuillermoORCID iD iconorcid.org/0000-0002-4987-7669
Alternative names
Publications (10 of 34) Show all publications
Bakhshi Valojerdi, Z. & Rodriguez-Navas, G. (2019). A Preliminary Roadmap for Dependability Research in Fog Computing. In: : . Paper presented at 17th International Workshop on Real-Time Networks – RTN 2019, Stuttgart, Germany, July 9, 2019, In conjunction with the 31st ECRTS.
Open this publication in new window or tab >>A Preliminary Roadmap for Dependability Research in Fog Computing
2019 (English)Conference paper, Published paper (Refereed)
Abstract [en]

Fog computing aims to support novel real-time applications byextending cloud resources to the network edge. This technologyis highly heterogeneous and comprises a wide variety of devicesinterconnected through the so-called fog layer. Compared to tra-ditional cloud infrastructure, fog presents more varied reliabilitychallenges, due to its constrained resources and mobility of nodes.This paper summarizes current research efforts on fault toleranceand dependability in fog computing and identifies less investigatedopen problems, which constitute interesting research directions tomake fogs more dependable.

National Category
Computer Systems Embedded Systems
Identifiers
urn:nbn:se:mdh:diva-45153 (URN)
Conference
17th International Workshop on Real-Time Networks – RTN 2019, Stuttgart, Germany, July 9, 2019, In conjunction with the 31st ECRTS
Available from: 2019-09-03 Created: 2019-09-03 Last updated: 2019-09-04Bibliographically approved
Filipovikj, P., Rodriguez-Navas, G. & Seceleanu, C. (2019). Bounded Invariance Checking of Simulink Models. In: Proceedings of the ACM Symposium on Applied Computing: . Paper presented at SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019 (pp. 2168-2177). , Part F147772
Open this publication in new window or tab >>Bounded Invariance Checking of Simulink Models
2019 (English)In: Proceedings of the ACM Symposium on Applied Computing, 2019, Vol. Part F147772, p. 2168-2177Conference paper, Published paper (Refereed)
Abstract [en]

Currently, Simulink models can be verified rigorously against design errors or statistical properties. In this paper, we show how Simulink models can be formally analyzed against invariance properties using bounded model checking reduced to satisfiability modulo theories solving. In its basic form, the technique provides means for verification of an underlying model over bounded traces rigorously, however, in general the procedure is incomplete. We identify common Simulink block types and compositions by analyzing selected industrial models, and we show that for some of them the set of non-repeating states (reachability diameter) can be visited with a finite set of paths of finite length, yielding the verification complete. We complement our approach with a tool, called SyMC that automates the following: i) calculation of the reachability diameter size for some of the designs, ii) generation of finite (bounded) paths of the underlying Simulink model and their encoding into SMT-LIB format and iii) checking invariance properties using the Z3 SMT solver. To show the applicability of our approach, we apply it on a prototype implementation of an industrial Simulink model, namely Brake by Wire from Volvo Group Trucks Technology, Sweden. 

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-42803 (URN)10.1145/3297280.3297493 (DOI)000474685800302 ()2-s2.0-85065663281 (Scopus ID)
Conference
SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019
Available from: 2019-02-27 Created: 2019-02-27 Last updated: 2019-10-11Bibliographically approved
Bakhshi Valojerdi, Z., Rodriguez-Navas, G. & Hansson, H. (2019). Dependable Fog Computing: A Systematic Literature Review. In: : . Paper presented at SEAA 2019 : 45th EUROMICRO SEAA Conference, Aug 28, 2019 - Aug 30, 2019, Thessaloniki / Chalkidiki, Greece.
Open this publication in new window or tab >>Dependable Fog Computing: A Systematic Literature Review
2019 (English)Conference paper, Published paper (Refereed)
Abstract [en]

Fog computing has been recently introduced to bridge the gap between cloud resources and the network edge. Fog enables low latency and location awareness, which is considered instrumental for the realization of IoT, but also faces reliability and dependability issues due to node mobility and resource constraints. This paper focuses on the latter, and surveys the state of the art concerning dependability and fog computing, by means of a systematic literature review. Our findings show the growing interest in the topic but the relative immaturity of the technology, without any leading research group. Two problems have attracted special interest: guaranteeing reliable data storage/collection in systems with unreliable and untrusted nodes, and guaranteeing efficient task allocation in the presence of varying computing load. Redundancy-based techniques, both static and dynamic, dominate the architectures of such systems. Reliability, availability and QoS are the most important dependability requirements for fog, whereas aspects such as safety and security, and their important interplay, have not been investigated in depth.

National Category
Computer Systems Embedded Systems
Identifiers
urn:nbn:se:mdh:diva-45152 (URN)
Conference
SEAA 2019 : 45th EUROMICRO SEAA Conference, Aug 28, 2019 - Aug 30, 2019, Thessaloniki / Chalkidiki, Greece
Available from: 2019-09-03 Created: 2019-09-03 Last updated: 2019-09-04Bibliographically approved
Pozo Pérez, F. M., Rodriguez-Navas, G. & Hansson, H. (2019). Methods for large-scale time-triggered network scheduling. Electronics (Switzerland), 8(7), Article ID 738.
Open this publication in new window or tab >>Methods for large-scale time-triggered network scheduling
2019 (English)In: Electronics (Switzerland), ISSN 2079-9292, Vol. 8, no 7, article id 738Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
MDPI AG, 2019
Keywords
Cyber-physical systems, Real-time networks, Scheduling, SMT solvers, Time-triggered
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-45101 (URN)10.3390/electronics8070738 (DOI)000482063200063 ()2-s2.0-85070718684 (Scopus ID)
Available from: 2019-08-28 Created: 2019-08-28 Last updated: 2019-09-12Bibliographically approved
Pozo Pérez, F. M., Rodriguez-Navas, G. & Hansson, H. (2019). Schedule reparability: Enhancing time-triggered network recovery upon link failures. In: Proceedings - 2018 IEEE 24th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2018: . Paper presented at 24th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2018; Hakodate; Japan; 29 August 2018 through 31 August 2018 (pp. 147-156). Institute of Electrical and Electronics Engineers Inc.
Open this publication in new window or tab >>Schedule reparability: Enhancing time-triggered network recovery upon link failures
2019 (English)In: Proceedings - 2018 IEEE 24th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2018, Institute of Electrical and Electronics Engineers Inc. , 2019, p. 147-156Conference paper, Published paper (Refereed)
Abstract [en]

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. 

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc., 2019
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-42810 (URN)10.1109/RTCSA.2018.00026 (DOI)000458980300017 ()2-s2.0-85061771050 (Scopus ID)9781538677599 (ISBN)
Conference
24th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2018; Hakodate; Japan; 29 August 2018 through 31 August 2018
Available from: 2019-02-28 Created: 2019-02-28 Last updated: 2019-09-06Bibliographically approved
Pozo Pérez, F. M., Rodriguez-Navas, G. & Hansson, H. (2019). Semi-Distributed Self-Healing Protocol for Online Schedule Repair after Network Failures.
Open this publication in new window or tab >>Semi-Distributed Self-Healing Protocol for Online Schedule Repair after Network Failures
2019 (English)Report (Other academic)
Abstract [en]

Adaptive requirements for networks with strict timing restrictions do challenge the static nature of the time-triggered communication paradigm. Continuous changes in the network topology during operation require frequent rescheduling, followed by schedule distribution, a process that is excessively time-consuming as it was intended to be performed only during the design phase. The fully-distributed Self-Healing Protocol introduced a collaborative method to quickly modify the local schedules of the nodes during runtime, after link failures. This protocol gets the network back to correct operation in milliseconds, but it assumes that only the nodes are able to modify their local schedules, which limited the achieved improvement. This paper proposes to shift to a semi-distributed strategy, where high-performance nodes are responsible for the nodes and links within a small network segment. These nodes rely on their privileged view of the system in order to reduce the response time, increase the healing success rate, and extend the fault model to include switch failures. 

National Category
Communication Systems
Identifiers
urn:nbn:se:mdh:diva-45162 (URN)
Available from: 2019-09-06 Created: 2019-09-06 Last updated: 2019-09-13Bibliographically approved
Filipovikj, P., Rodriguez-Navas, G. & Seceleanu, C. (2018). Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience. Electronic Communications of the EASST, 75, 1-20
Open this publication in new window or tab >>Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience
2018 (English)In: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 75, p. 1-20Article in journal (Refereed) Published
Abstract [en]

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

Place, publisher, year, edition, pages
Germany: , 2018
Keywords
SMT-based consistency analysis, model-checking-based consistency analysis
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41726 (URN)10.14279/tuj.eceasst.75 (DOI)ISSN 1863-2122 (ISBN)
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2018-12-20 Created: 2018-12-20 Last updated: 2018-12-20Bibliographically approved
Mahmud, N., Rodriguez-Navas, G., Faragardi, H. R., Mubeen, S. & Seceleanu, C. (2018). Power-aware Allocation of Fault-tolerant Multi-rate AUTOSAR Applications. In: 25th Asia-Pacific Software Engineering Conference APSEC'18: . Paper presented at 25th Asia-Pacific Software Engineering Conference APSEC'18, 04 Dec 2018, Nara, Japan.
Open this publication in new window or tab >>Power-aware Allocation of Fault-tolerant Multi-rate AUTOSAR Applications
Show others...
2018 (English)In: 25th Asia-Pacific Software Engineering Conference APSEC'18, 2018Conference paper, Published paper (Refereed)
Abstract [en]

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.

Keywords
autosar, software allocation, optimization, power consumption, distributed architecture, multi-rate systems, timing, reliability
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-43902 (URN)10.1109/APSEC.2018.00034 (DOI)000474770300021 ()2-s2.0-85066797560 (Scopus ID)
Conference
25th Asia-Pacific Software Engineering Conference APSEC'18, 04 Dec 2018, Nara, Japan
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyDPAC - Dependable Platforms for Autonomous systems and Control
Available from: 2019-06-14 Created: 2019-06-14 Last updated: 2019-10-11Bibliographically approved
Zamansky, A., Spichkova, M., Rodriguez-Navas, G., Herrmann, P. & Blech, J. O. (2018). Towards classification of lightweight formal methods. In: ENASE 2018 - Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering: . Paper presented at 13th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2018, 23 March 2018 through 24 March 2018 (pp. 305-313). SciTePress
Open this publication in new window or tab >>Towards classification of lightweight formal methods
Show others...
2018 (English)In: ENASE 2018 - Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, SciTePress , 2018, p. 305-313Conference paper, Published paper (Refereed)
Abstract [en]

The use of lightweight formal methods (LFM) for the development of industrial applications has become a major trend. Although the term “lightweight formal methods” has been used for over ten years now, there seems to be no common agreement on what “lightweight” actually means, and different communities apply the term in all kinds of ways. In this paper, we explore the recent trends in the use of LFM, and establish our opinion that cost-effectiveness is the driving force to deploy LFM. Further, we propose a simple framework that should help to classify different LFM approaches and to estimate which of them are most cost-effective for a certain software engineering project. We demonstrate our framework using some examples. 

Place, publisher, year, edition, pages
SciTePress, 2018
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-40923 (URN)10.5220/0006770803050313 (DOI)000450506700029 ()2-s2.0-85052811918 (Scopus ID)9789897583001 (ISBN)
Conference
13th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2018, 23 March 2018 through 24 March 2018
Available from: 2018-09-13 Created: 2018-09-13 Last updated: 2018-12-27Bibliographically approved
Pozo, F., Rodriguez-Navas, G. & Hansson, H. (2018). Work-in-Progress: A Hot-Patching Protocol for Repairing Time-Triggered Network Schedules. In: Pellizzoni, R (Ed.), 24TH IEEE REAL-TIME AND EMBEDDED TECHNOLOGY AND APPLICATIONS SYMPOSIUM (RTAS 2018): . Paper presented at 24th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), APR 11-13, 2018, Porto, PORTUGAL (pp. 89-92).
Open this publication in new window or tab >>Work-in-Progress: A Hot-Patching Protocol for Repairing Time-Triggered Network Schedules
2018 (English)In: 24TH IEEE REAL-TIME AND EMBEDDED TECHNOLOGY AND APPLICATIONS SYMPOSIUM (RTAS 2018) / [ed] Pellizzoni, R, 2018, p. 89-92Conference paper, Published paper (Refereed)
Abstract [en]

Time-Triggered communication is based on generating an offfine static schedule that guarantees frame transmissions with reduced latency and low jitter. However, static schedules are not adaptive: if some unpredicted event happens, like a link failure, the schedule is not valid anymore and a new one needs to be synthesized from scratch. This paper presents a novel hot-patching protocol which seeks, after a link failure disconnecting two nodes, to find a new path to reconnect both nodes and restore during run-time the affected part of the schedule. We also introduce the concept of reparability as a desired property of the schedule, which increases the probability of our protocol to succeed. The first evaluation shows that our hot-patching protocol can recover from a link failure consistently in less than 25ms.

Series
IEEE Real-Time and Embedded Technology and Applications Symposium, ISSN 1545-3421
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-40937 (URN)10.1109/RTAS.2018.00015 (DOI)000443421100009 ()2-s2.0-85058458750 (Scopus ID)978-1-5386-5295-4 (ISBN)
Conference
24th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), APR 11-13, 2018, Porto, PORTUGAL
Available from: 2018-09-13 Created: 2018-09-13 Last updated: 2019-01-04Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-4987-7669

Search in DiVA

Show all publications