mdh.sePublications
Change search
Refine search result
1 - 37 of 37
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Alorda, B.
    et al.
    Electronic System Group, Illes Balears University, Spain .
    Pujol-Nadal, R.
    Physics Department, Illes Balears University, Spain.
    Rodriguez-Navas, G.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Mathematics and Computer Science Dept, Illes Balears University, Spain .
    Moià-Pol, A.
    Physics Department, Illes Balears University, Spain .
    Martínez-Moll, V.
    Physics Department, Illes Balears University, Spain .
    Collaborative distributed sun-tracking control system for building integration with minimal plant area and maximum energy-conversion efficiency2015In: International Journal of Electrical Power & Energy Systems, ISSN 0142-0615, E-ISSN 1879-3517, Vol. 70, p. 52-60Article in journal (Refereed)
    Abstract [en]

    This paper presents a collaborative distributed sun-tracking control system for a novel Fixed Mirror Solar Concentrator (FMSC) structure, which increases the energy-conversion efficiency of the FMSC and reduces the space between solar collectors units, a positive aspect for in-building integration. The improved FMSC uses solar concentration collectors suited for mid-range thermal applications (90-200 °C) and is designed for easy installation in buildings because of its relatively small extension. The proposed solar orientation system (ORSYS) relies on a two-step algorithm to increase the energy captured by the receiver, which provides tolerance to common logical and mechanical errors in the estimation of the receiver position. ORSYS is implemented as a CAN-based distributed system, extended with web-interface features for supervision and configuration of the overall system. ORSYS also includes a coordination algorithm that allows adjacent collectors to share the physical space between them, thus reducing the total plant area. Experimental evaluation has been performed using an industrial-scale solar collector prototype, showing its feasibility and efficiency in terms of energy conversion in real environments.

  • 2.
    Ashjaei, Mohammad
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Behnam, Moris
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Universitat de les Illes Balears, Spain.
    Nolte, Thomas
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Implementing a Clock Synchronization Protocol on a Multi-Master Switched Ethernet Network2013Conference paper (Refereed)
    Abstract [en]

    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.

  • 3.
    Avni, G.
    et al.
    IST Austria, Klosterneuburg, Austria.
    Goel, S.
    IIT Bombay, Mumbai, India.
    Henzinger, T. A.
    IST Austria, Klosterneuburg, Austria.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Computing scores of forwarding schemes in switched networks with probabilistic faults2017In: Lecture Notes in Computer Science, Volume 10206, Springer Verlag , 2017, p. 169-187Conference paper (Refereed)
    Abstract [en]

    Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability. We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant ℓ, we compute the score of the scheme, namely the probability (induced by faults) that at least ℓ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a “product-like” structure. Its special structure allows us to reason about it symbolically, and reduce the scoring problem to #SAT. Our solution is generic and can be adapted to different networks and other contexts. Also, we show the computational complexity of the scoring problem is #P-complete, and we study methods to estimate the score. We evaluate the effectiveness of our techniques with an implementation.

  • 4.
    Avni, G.
    et al.
    IST Austria, Klosterneuburg, Austria..
    Guha, S.
    Hebrew Univ Jerusalem, Jerusalem, Israel.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Synthesizing time-triggered schedules for switched networks with faulty links2016In: Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016, 2016, article id a26Conference paper (Refereed)
    Abstract [en]

    Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation.

  • 5.
    Bakhshi Valojerdi, Zeinab
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Nokia Bell Labs, Israel.
    A Preliminary Roadmap for Dependability Research in Fog Computing2019Conference 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.

  • 6.
    Bakhshi Valojerdi, Zeinab
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Dependable Fog Computing: A Systematic Literature Review2019Conference 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.

  • 7.
    Ballesteros, A.
    et al.
    DMI, Universitat de les Illes Balears, Spain.
    Proenza, J.
    DMI, Universitat de les Illes Balears, Spain.
    Gessner, D.
    DMI, Universitat de les Illes Balears, Spain.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Sauter, T.
    Danube University Krems, Austria.
    Achieving elementary cycle synchronization between masters in the flexible time-triggered replicated star for ethernet2014In: 19th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2014, 2014, p. Article number 7005335-Conference paper (Refereed)
    Abstract [en]

    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.

  • 8.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Jagerfield, Trevor
    Mälardalen University.
    Nyberg, Mattias
    Scania, Södertälje, Sweden.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain2016In: PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2, 2016, Vol. 2, p. 167-173, article id 7552198Conference paper (Refereed)
    Abstract [en]

    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.

  • 9.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mahmud, Nesredin
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Marinescu, Raluca
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Ljungkrantz, Oscar
    Volvo Group Trucks Technology, Gothenburg, Sweden.
    Lönn, Henrik
    Volvo Group Trucks Technology, Gothenburg, Sweden.
    Analyzing Industrial Simulink Models by Statistical Model Checking2017Report (Other academic)
    Abstract [en]

    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.

  • 10.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyberg, M.
    Scania, Södertälje, Sweden .
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings2014In: 2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings, 2014, p. 444-450Conference paper (Refereed)
    Abstract [en]

    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.

  • 11.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyberg, Mattias
    Scania, Sodertalje, Sweden..
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain2014In: 2014 IEEE 22ND INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE (RE), IEEE , 2014, p. 444-450Conference paper (Refereed)
    Abstract [en]

    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.

  • 12.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyberg, Mattias
    Scania AB CV, Södertälje, Sweden.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Automated SMT-based Consistency Checking of Industrial Critical Requirements2017In: ACM SIGAPP Applied Computing Review, ISSN 1559-6915, E-ISSN 1931-0161, Vol. 17, no 4, p. 15-28Article in journal (Refereed)
    Abstract [en]

    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.

  • 13.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyberg, Mattias
    Scania, Sweden.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    SMT-based Consistency Analysis of Industrial Systems Requirements2017In: 32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 2017, Vol. F128005, p. 1272-1279Conference paper (Refereed)
    Abstract [en]

    As the complexity of industrial systems increases, it becomes dificult to ensure the correctness of system requirements specifications with respect to certain criteria such as consistency. Automated techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. However, such approaches can some-times be costly in terms of modeling and analysis time or not applicable for certain types of properties. In this paper, we present a complementary method that relies on pattern-based formalization of requirements and automated consistency checking using the state-of-the-art SMT tool Z3. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive subsystem called the Fuel Level Display. 

  • 14.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Bounded Invariance Checking of Simulink Models2019In: Proceedings of the ACM Symposium on Applied Computing, 2019, Vol. Part F147772, p. 2168-2177Conference 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. 

  • 15.
    Filipovikj, Predrag
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience2018In: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 75, p. 1-20Article in journal (Refereed)
    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.

  • 16.
    Mahmud, Nesredin
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Faragardi, Hamid Reza
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Mubeen, Saad
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Power-aware Allocation of Fault-tolerant Multi-rate AUTOSAR Applications2018In: 25th Asia-Pacific Software Engineering Conference APSEC'18, 2018Conference 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.

  • 17.
    Pozo, Francisco
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, G.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
    Hansson, Hans A
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
    Steiner, Wilfried
    TTTech Computertechnik AG.
    Schedule Synthesis for Next Generation Time-Triggered Networks2017Report (Other academic)
    Abstract [en]

    For handling frame transmissions in highly deterministic real-time networks, i.e. networks requiring low communication latency and minimal jitter, an offline time-triggered schedule indicating the dispatch times of all frames can be used. Generation of such an offline schedule is known to be a NPcomplete problem, with complexity driven by the size of the network, the number and complexity of the traffic temporal constraints, and link diversity (for instance, coexistence of wired and wireless links). As embedded applications become more complex and extend over larger geographical areas, there is a need to deploy larger real-time networks, but existing schedule synthesis mechanisms do not scale satisfactorily to the sizes of these networks, constituting a potential bottleneck for system designers. In this paper, we present an offline synthesis tool that overcomes this limitation and is capable of generating time-triggered schedules for networks with hundreds of nodes and thousands of temporal constraints, also for systems where wired and wireless links are combined. This tool models the problem with linear arithmetic constraints and solves them using a Satisfiability Modulo Theory (SMT) solver, a powerful general purpose tool successfully used in the past for synthesizing time-triggered schedules. To cope with complexity, our algorithm implements a segmented approach that divides the total problem into easily solvable smaller-size scheduling problems, whose solutions can be combined for achieving the final schedule. The paper also discusses a number of optimizations that increase the size and compactness of the solvable schedules. We evaluate our approach on a set of realistic large-size multi-hop networks, significantly bigger than those in the existing literature. The results show that our segmentation reduces the synthesis time dramatically, allowing generation of extremely large compact schedules.

  • 18.
    Pozo, Francisco
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Self-Healing Protocol: Repairing Scheduels Online after Link Failures in Time-Triggered NetworksIn: IEEE Transactions on Industrial Informatics, ISSN 1551-3203, E-ISSN 1941-0050Article in journal (Refereed)
    Abstract [en]

    The time-triggered paradigm is not adaptive, a static schedule determines the time-triggered communication and, then, any unpredicted change, like a link failure, might result in the loss of frames. Using spatial redundancy or recomputing a new schedule for replacement achieves fault tolerance only in moderate-size networks. With the increase in size and complexity of cyber-physical systems, more scalable and cost-efficient mechanisms are needed in order to complement conventional solutions. We propose a distributed Self-Healing Protocol that instead of recomputing the whole schedule, repairs the existent schedule at runtime. The basis of our protocol is the collaboration of nodes in the network to individually adjust their local schedules for rerouting the frames affected by link failures. Our protocol exhibits a high success rate compared to full rescheduling, as well as remarkable scalability; it repairs the schedule in milliseconds, whereas rescheduling requires minutes.

  • 19.
    Pozo, Francisco
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Work-in-Progress: A Hot-Patching Protocol for Repairing Time-Triggered Network Schedules2018In: 24TH IEEE REAL-TIME AND EMBEDDED TECHNOLOGY AND APPLICATIONS SYMPOSIUM (RTAS 2018) / [ed] Pellizzoni, R, 2018, p. 89-92Conference 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.

  • 20.
    Pozo, Francisco
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Steiner, W.
    TTTech Computertechnik AG, Vienna, Austria .
    SMT-based synthesis of TTEthernet schedules: A performance study2015In: 2015 10th IEEE International Symposium on Industrial Embedded Systems, SIES 2015 - Proceedings, 2015, p. 162-165Conference paper (Refereed)
    Abstract [en]

    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.

  • 21.
    Pozo, Francisco
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Steiner, W.
    TTTech Computertechnik AG, Vienna, Austria.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Period-Aware Segmented Synthesis of Schedules for Multi-Hop Time-Triggered Networks2016In: 22nd IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2016), IEEE, 2016, p. 170-175Conference paper (Refereed)
    Abstract [en]

    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.

  • 22.
    Pozo, Francisco
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Steiner, W.
    TTTech Computertechnik AG, Vienna, Austria.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    A decomposition approach for SMT-based schedule synthesis for time-triggered networks2015In: 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA), 2015, p. Article number 7301436-Conference paper (Refereed)
    Abstract [en]

    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.

  • 23.
    Pozo Pérez, Francisco Manuel
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Methods for large-scale time-triggered network scheduling2019In: Electronics (Switzerland), ISSN 2079-9292, Vol. 8, no 7, article id 738Article in journal (Refereed)
    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.

  • 24.
    Pozo Pérez, Francisco Manuel
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Schedule reparability: Enhancing time-triggered network recovery upon link failures2019In: 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 (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. 

  • 25.
    Pozo Pérez, Francisco Manuel
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Semi-Distributed Self-Healing Protocol for Online Schedule Repair after Network Failures2019Report (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. 

  • 26.
    Rodriguez-Navas, Guillermo
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Duboc, L.
    State University of Rio de Janeiro, Rio de Janeiro, Brazil .
    Betz, S.
    Karlsruhe Institute for Technology, Karlsruhe, Germany .
    Chitchyan, R.
    University of Leicester, Leicester, United Kingdom .
    Penzenstadler, B.
    California State University, Long Beach, CA, United States .
    Venters, C. C.
    University of Huddersfield, Huddersfield, United Kingdom .
    Safety vs. sustainability design: Analogies, differences and potential synergies2015In: CEUR Workshop Proceedings, 2015, p. 25-34Conference paper (Refereed)
    Abstract [en]

    The idea that there are important parallels between safety and sustainability and that software engineers might be able to take lessons learned from safety and apply them to sustainability has been voiced and initially explored before. This paper extends the analysis of similarities, differences, and potential synergies between the two concepts, according to four different dimensions of these domains: systemicity, complexity, certification and social perception. Copyright © 2015 for this paper by its authors. Copying permitted for private and academic purposes.

  • 27.
    Rodriguez-Navas, Guillermo
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Graydon, Patrick
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Bate, Iain
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Dept. of Computer Science, University of York, United Kingdom.
    From fault injection to mutant injection: The next step for safety analysis?2013In: Lect. Notes Comput. Sci., 2013, p. 276-277Conference paper (Refereed)
    Abstract [en]

    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.

  • 28.
    Rodriguez-Navas, Guillermo
    et al.
    Universitat de les Illes Balears, Spain.
    Hansson, Hans
    Mälardalen University, Department of Computer Science and Electronics.
    An UPPAAL Model for Formal Verification of Master/Slave Clock2006In: Factory Communication Systems, 2006 IEEE International Workshop on, 2006, p. 3-12Conference paper (Refereed)
    Abstract [en]

    Many distributed applications require a clock synchronization service. We have previously proposed a clock synchronization service for the Controller Area Network (CAN), which we have claimed to provide highly synchronized clocks even in the occurrence of faults in the system. In this paper we substantiate this claim by providing a formal model and verification of our fault tolerant clock synchronization mechanism. We base our modeling and verification on timed automata theory as implemented by the model checking tool UPPAAL. In the modeling we introduce a novel technique for modeling drifting clocks. The verification shows that a precision in the order of 2 μs is guaranteed despite node’s faults as well as consistent channel faults. It also shows that inconsistent channel faults may significantly worsen the achievable precision, but that this effect can be reduced by choosing a suitable resynchronization period.

  • 29.
    Rodriguez-Navas, Guillermo
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Kobetski, Avenir
    Swedish Institute of Computer Science Kista, Sweden.
    Sundmark, Daniel
    Swedish Institute of Computer Science Kista, Sweden.
    Gustafsson, Thomas
    Scania CV AB Södertälje, Sweden.
    Offline Analysis of Independent Guarded Assertions in Automotive Integration Testing2015In: Proceedings - 2015 IEEE 17th International Conference on High Performance Computing and Communications, 2015 IEEE 7th International Symposium on Cyberspace Safety and Security and 2015 IEEE 12th International Conference on Embedded Software and Systems, HPCC-CSS-ICESS 2015, 2015, p. 1066-1073Conference paper (Refereed)
    Abstract [en]

    The size and complexity of software in automotive systems have increased steadily over the last decades. Modern vehicles typically contain numerous electrical control units (ECUs), and more and more features require real-time interaction between several dedicated ECUs (e.g., gearbox, brake and engine control units) in order to perform their tasks. Since system safety and reliability must not be adversely affected by this increase in complexity, proper quality assurance is a must. Such quality assurance is often performed by testing the system in different levels of integration throughout the development process. However, the growth of complexity of the system under test aslo affects the testing, making it laborious, difficult and costly. This paper presents a novel method for efficient offline analysis of traces, which has been especially tailored for integration testing of automotive systems. The method exploits the recently defined concept of independent guarded assertion in order to formally describe the events that are relevant for the analysis as well as the expected behavior in those events. The offline analysis is implemented using a standard commercial model checker and has shown good performance in the conducted experiments.

  • 30.
    Rodriguez-Navas, Guillermo
    et al.
    Universitat de les Illes Balears, Spain.
    Proenza, Julian
    Universitat de les Illes Balears, Spain.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering.
    Pettersson, Paul
    Mälardalen University, School of Innovation, Design and Engineering.
    Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems2010In: Behavioral Modeling for Embedded Systems and Technologies: Applications for Design and Implementation, IGI Global, 2010, p. 172-193Chapter in book (Other academic)
    Abstract [en]

    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.

  • 31.
    Rodriguez-Navas, Guillermo
    et al.
    Mälardalen University, School of Innovation, Design and Engineering.
    Ribot, Miquel A.
    Universitat de Les Illes Balears, Spain.
    Alorda, Bartomeu
    Universitat de Les Illes Balears, Spain.
    Understanding the Role of Transmission Power in Component-Based Architectures for Adaptive WSN2012In: Proceedings - International Computer Software and Applications Conference, 2012, p. 520-525Conference paper (Refereed)
    Abstract [en]

    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.

  • 32.
    Rodriguez-Navas, Guillermo
    et al.
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Scania SV, Södertäalje, Sweden .
    Seceleanu, Cristina
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Hansson, Hans
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Nyberg, M.
    Scania SV, Södertäalje, Sweden .
    Ljungkrantz, O.
    Advanced Technology and Research, Volvo Group Trucks Technology, Gothenburg, Sweden .
    Lönn, H.
    Advanced Technology and Research, Volvo Group Trucks Technology, Gothenburg, Sweden .
    Automated specification and verification of functional safety in heavy-vehicles: The verispec approach2014In: Proceedings - Design Automation Conference, 2014Conference paper (Refereed)
    Abstract [en]

    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.

  • 33.
    Steiner, Wilfried
    et al.
    TTTech Computertechnik AG, Austria.
    Gutiérrez, Marina
    TTTech Computertechnik AG, Austria.
    Matyas, Zoltan
    TTTech Hungary Kft., Budapest, Hungary.
    Pozo Pérez, Francisco Manuel
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Current Techniques, Trends and New Horizons In Avionics Networks Configuration2015In: Digital Avionics Systems Conference DASC-34, 2015Conference paper (Other academic)
  • 34.
    Steiner, Wilfried
    et al.
    TTTech Computertechnik AG, Austria.
    Gutiérrez Peón, Pablo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. TTTech Computertechnik AG, Austria.
    Gutiérrez, Marina
    TTTech Computertechnik AG, Austria.
    Mehmed, Ayhan
    TTTech Computertechnik AG, Austria.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Lisova, Elena
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Pozo Pérez, Francisco Manuel
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Next Generation Real-Time Networks Based on IT Technologies2016In: 21st IEEE Conference on Emerging Technologies and Factory Automation ETFA'16, 2016, p. Article number 7733580-Conference paper (Refereed)
    Abstract [en]

    Ethernet-based networks have found their way into industrial communication more than a decade ago. However, while industry and academia developed Ethernet variants to also meet real-time and fault-tolerant requirements, recent standardization efforts within the IEEE 802 will broadly bring standard IT switched Ethernet in future industrial communication networks. As first standards of IEEE 802.1 time-sensitive networking (TSN) are becoming published at the time of this writing, we review these standards and formulate further research challenges that still go beyond current standard developments. Furthermore, we report on recent research results from the RetNet project that target these research challenges.

  • 35.
    Venters, Colin C.
    et al.
    University of Huddersfield, UK.
    Becker, Christoph
    University of Toronto, Canada.
    Betz, Stefanie
    Karlsruhe Institute for Technology, Germany.
    Chitchyan, Ruzanna
    University of Leicester, UK.
    Duboc, Leticia
    State University of Rio de Janeiro, Brasil.
    Easterbrook, Steve
    University of Toronto, Canada.
    Penzenstadler, Birgit
    California State University Long Beach, USA.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Seyff, Norbert
    University of Zurich, Switzerland.
    Mind the Gap: Bridging the Sustainable Software Systems Research Divide2015In: Workshop on Sustainable HCI in the UK UK-SHCI, 2015Conference paper (Refereed)
    Abstract [en]

    Sustainability is a major concern to humanity as a result of the consequences of the rapid consumption of the planets finite natural resources, combined with exponential economic and population growth. Principally associated with the field of ecology, sustainability has emerged as an important area of research in a number of sub-fields within the domain of computing including human-computer interaction. While these communities have attempted to address the challenges of sustainability from their different perspectives, there is a severe lack of common understanding of the fundamental concepts of sustainability and how they relate to software systems. As a result, there is a need for a common ground and consistent terminology to reduce the replication of effort. This paper presents the Karlskrona Manifesto for Sustainabilty Design as a mechanism for initiating a conversation between the different communities in addressing the challenges of developing sustainable software systems.

  • 36.
    Zamansky, A.
    et al.
    University of Haifa, Carmel Mountain, Haifa, Israel .
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Adams, M.
    Proof Technologies Ltd., Worcester, United Kingdom.
    Spichkova, M.
    RMIT University, Melbourne, Australia .
    Formal methods in collaborative projects2016In: ENASE 2016 - Proceedings of the 11th International Conference on Evaluation of Novel Software Approaches to Software Engineering, 2016, p. 396-402Conference paper (Refereed)
    Abstract [en]

    In this paper we address particular aspects of integration of formal methods in large-scale industrial projects, namely collaborative aspects. We review recent works addressing such aspects, identify some current trends and discuss directions for further research. 

  • 37.
    Zamansky, A.
    et al.
    University of Haifa, Haifa, Israel.
    Spichkova, M.
    RMIT University, Melbourne, Australia.
    Rodriguez-Navas, Guillermo
    Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
    Herrmann, P.
    Norwegian University of Science and Technology, Trondheim, Norway.
    Blech, J. O.
    BHTC GmbH, Lippstadt, Germany.
    Towards classification of lightweight formal methods2018In: ENASE 2018 - Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, SciTePress , 2018, p. 305-313Conference 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. 

1 - 37 of 37
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf