| 1. |
- Ashjaei, Mohammad, et al.
(författare)
-
Implementing a Clock Synchronization Protocol on a Multi-Master Switched Ethernet Network
- 2013
-
Konferensbidrag (refereegranskat)abstract
- The interest to use Switched Ethernet technologies in real-time communication is increasing due to its absence of collisions when transmitting messages. Nevertheless, using COTS switches affect the timeliness guarantee inherent in potentially overflowing internal FIFO queues. In this paper we focus on a solution, called the FTT-SE protocol, which is developed based on a master-slave technique. Recently, an extension of the FTT-SE protocol has been proposed where the transmission of messages are controlled using multiple master nodes. In order to guarantee the correctness of the protocol, the masters should be timely synchronized. Therefore, in this paper we investigate using a clock synchronization protocol, based on the IEEE 1588 standard, among master nodes and we study the effects of this protocol on the network performance. In addition, we present a formal verification of this solution by means of model checking to prove the correctness of the FTT-SE protocol when the clock synchronization protocol is applied.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
| 4. |
- Filipovikj, Predrag, et al.
(författare)
-
Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain
- 2014
-
Ingår i: 2014 IEEE 22ND INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE (RE). - : IEEE. - 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.
|
|
| 5. |
- Rodriguez-Navas, Guillermo, et al.
(författare)
-
Automated specification and verification of functional safety in heavy-vehicles : The verispec approach
- 2014
-
Ingår i: Proceedings - Design Automation Conference. - New York, NY, USA : ACM. - 9781479930173
-
Konferensbidrag (refereegranskat)abstract
- ISO 26262 is the new standard for automotive functional safety. This standard identies major process steps across a large number of system stages as well as safety-related artifacts required as input and output of these steps. The VeriSpec project intends to identify the main challenges for the adoption of ISO 26262 by the heavy-vehicle industry and to provide useful and industrially relevant components (methods, tools etc.) required by the standard. The project work targets two main research goals: (i) requirement formalization support, including a usable front-end for specifying requirements by using patterns, and (ii) formal analysis of realizations in form of architectural models at various levels of abstraction, by model-checking the formal representations of the latter. In this paper, we present the current challenges facing industry and justifying VeriSpec, together with a preliminary roadmap for the research.
|
|
| 6. |
- Rodriguez-Navas, Guillermo, et al.
(författare)
-
From fault injection to mutant injection : The next step for safety analysis?
- 2013
-
Ingår i: Lect. Notes Comput. Sci.. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783642396106 ; , s. 276-277
-
Konferensbidrag (refereegranskat)abstract
- Mutation testing has been used to assess test suite coverage, and researchers have proposed adapting the idea for other uses. Safety kernels allow the use of untrusted software components in safety-critical applications: a trusted software safety kernel detects undesired behavior and takes remedial action. We propose to use specification mutation, model checking, and model-based testing to verify safety kernels for component-based, safety-critical computer systems.
|
|
| 7. |
- Rodriguez-Navas, Guillermo, et al.
(författare)
-
Understanding the Role of Transmission Power in Component-Based Architectures for Adaptive WSN
- 2012
-
Ingår i: Proceedings - International Computer Software and Applications Conference. - 9780769547589 ; , s. 520-525
-
Konferensbidrag (refereegranskat)abstract
- Component-based architectures can play an important role in solving some of the problems related to energy management in Wireless Sensor Networks. It has been recently shown that real-time interfaces, and their associated mechanisms for online adaptation, are useful for solving the problem of dynamically allocating bandwidth in a WSN, while still satisfying both quality and energy constraints. In this paper we will discuss the relevance of extending this model with a new parameter, the transmission power of the nodes. Based on experimental data, it will be shown that this parameter has a strong impact on both the energy consumed by the nodes and the quality/reliability of the communication. The integration of this feature with the notion real-time interface, although not completely solved, will be discussed as well.
|
|
| 8. |
- Rodriguez-Navas, Guillermo, et al.
(författare)
-
Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems
- 2010
-
Ingår i: Behavioral Modeling for Embedded Systems and Technologies. - : IGI Global. - 9781605667508 ; , s. 172-193
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Model checking is a widely used technique for the formal verification of computer systems. However, the suitability of model checking strongly depends on the capacity of the system designer to specify a model that captures the real behaviour of the system under verification. For the case of real-time systems, this means being able to realistically specify not only the functional aspects, but also the temporal behaviour of the system. This chapter is dedicated to modeling clocks in distributed embedded systems using the timed automata formalism. The different types of computer clocks that may be used in a distributed embedded system and their effects on the temporal behaviour of the system are introduced, together with a systematic presentation of how the behaviour of each kind of clock can be modeled. The modeling is particularized for the UPPAAL model checker, although it can be easily adapted to other model checkers based on the theory of timed automata.
|
|
