Weighted automata are a generalization of nondeterministic automata that associate a weight drawn from a semiring $K$ with every transition and every state. Their behaviours can be formalized either as weighted language equivalence or weighted bisimulation. In this paper we explore the properties of weighted automata in the framework of coalgebras over (i) the category $\mathsf{SMod}$ of semimodules over a semiring $K$ and $K$-linear maps, and (ii) the category $\mathsf{Set}$ of sets and maps. We show that the behavioural equivalences defined by the corresponding final coalgebras in these two cases characterize weighted language equivalence and weighted bisimulation, respectively. These results extend earlier work by Bonchi et al. using the category $\mathsf{Vect}$ of vector spaces and linear maps as the underlying model for weighted automata with weights drawn from a field $K$. The key step in our work is generalizing the notions of linear relation and linear bisimulation of Boreale from vector spaces to semimodules using the concept of the kernel of a $K$-linear map in the sense of universal algebra. We also provide an abstract procedure for forward partition refinement for computing weighted language equivalence. Since for weighted automata defined over semirings the problem is undecidable in general, it is guaranteed to halt only in special cases. We provide sufficient conditions for the termination of our procedure. Although the results are similar to those of Bonchi et al., many of our proofs are new, especially those about the coalgebra in $\mathsf{SMod}$ characterizing weighted language equivalence.

Path‐based equivalence checkers (PBECs) have been successfully applied for verification of programmes from diverse domains and from various stages of high‐level synthesis. In the case of non‐equivalence, PBEC provides very little information which is not sufficient for further investigation of the two programmes being compared by some human expert. In this work, the authors show how a counter‐trace ( cTrace ) can be generated in the case of non‐equivalence reported by the PBEC. Using this cTrace , they also present a procedure to find suitable initialisation values for input variables which reveal the non‐equivalence (i.e. counter‐example) by using off‐the‐shelf satisfiability modulo theories (SMT) solvers. To aid the human expert, they also show that how they can visualise this cTrace in the control and data‐flow graph of the programmes using the graph visualisation software – Graphviz. This counter‐example and visual representation of the corresponding cTrace will be helpful in debugging the root cause of the non‐equivalence. The experimental results are encouraging.

Translation validation is the process of proving that the target code is a correct translation of the source program being compiled. In this paper, we propose a translation validation method to verify code motion transformations involving loops applied during the scheduling phase of high-level synthesis (HLS). Our method is capable of ignoring false computations during translation validation. We have also identified a scenario involving code motion across loops where the state-of-the-art translation validation method gives false positive results. Our method can prove the nonequivalence of the concerned finite state machines with data paths in this scenario. We detected a bug in the HLS tool SPARK involving loop invariant code motion using our method. Experimental results demonstrate the usefulness of our method.

Real-time and embedded systems are moving from the traditional design paradigm to integration of multiple functionalities onto a single computing platform. Some of the functionalities are safety critical and subject to certification. The rest of the functionalities are nonsafety critical and do not need to be certified. Designing efficient scheduling algorithms which can be used to meet the certification requirement is challenging. Our research considers the time-triggered approach to scheduling of mixed-criticality jobs with two criticality levels. The first proposed algorithm for the time-triggered approach is based on the OCBP scheduling algorithm which finds a fixed-priority order of jobs. Based on this priority order, the existing algorithm constructs two scheduling tables S LO oc and S HI oc . The scheduler uses these tables to find a scheduling strategy. Another time-triggered algorithm called MCEDF was proposed as an improvement over the OCBP-based algorithm. Here we propose an algorithm which directly constructs two scheduling tables without using a priority order. Furthermore, we show that our algorithm schedules a strict superset of instances which can be scheduled by the OCBP-based algorithm as well as by MCEDF. We show that our algorithm outperforms both the OCBP-based algorithm and MCEDF in terms of the number of instances scheduled in a randomly generated set of instances. We generalize our algorithm for jobs with m criticality levels. Subsequently, we extend our algorithm to find scheduling tables for periodic and dependent jobs. Finally, we show that our algorithm is also applicable to mixed-criticality synchronous programs upon uniprocessor platforms and schedules a bigger set of instances than the existing algorithm.

In this paper we consider the case of a network of Electronic Control Units (ECUs) connected through a Flex Ray bus in the automotive domain. Multiple distributed applications can run on this underlying architecture, each partitioned into tasks that are mapped on different ECUs. These applications can often be executed in different functional modes with different requirements on the communication resources in terms of data size and sampling period. Moreover, new applications can be deployed on to the ECUs at run-time. To efficiently utilize the communication resources and accommodate new applications, a certain flexibility in reallocation of the resource is necessary. However, the Flex Ray bus requires static configuration of schedules and data mapping in order to guarantee a more deterministic system behavior, allowing little room for flexibility. In order to address this problem, we propose a reconfigurable communication middleware that lies between the application layer and the communication controller layer, which maps messages onto Flex Ray schedules, and can be reconfigured at runtime. The configuration is synthesized and deployed online, allowing a certain reallocation of communication resources to applications. In this paper, we describe the design of such a reconfigurable communication middleware and demonstrate its function with an implementation using industry-strength Flex Ray design tools.

The IEEE 802.11 standard for wireless local area networks defines a power management algorithm for Independent Basic Service Set (IBSS) allowing it to save critical battery energy in low powered wireless devices. The power management algorithm for IBSS uses beacon intervals (BIs) as the time unit, where every BI consists of an Announcement Traffic Indication Message (ATIM) window and a data window. The stations that have data to send need to go through a handshaking procedure in the ATIM window. If this handshaking is successful, the station remains awake in the data window and participates in the data communication. Otherwise, it goes into the sleep mode. This paper presents an analytical model to compute the throughput, expected delay and expected power consumption in an IEEE 802.11 IBSS in power save mode (PSM) for different traffic conditions in the network. The impact of data arrival rate, network size, and size of the BI on the performance of the IEEE 802.11 DCF in PSM is also analyzed. This analysis reveals a clear trade-off among throughput, delay, and average power consumption. The trade-off analysis is useful for designing efficient power consumption algorithms while maintaining the consistence performance of the network in terms of throughput and delay.

The SPEEDS project is aimed at making rich components models (RCM) into a mature framework in all phases of the design of complex distributed embedded systems. The RCM model is required to be expressive enough to cover the entire development process from requirements to code through design, and also capture both functional and non-functional aspects. In this paper we propose a language-based framework for real-time component interfaces in SPEEDS that is suitable at the ECU layer when a target processor has been identified, and WCET analysis done. We assume a discrete time model.

Modern real-time embedded systems are highly heterogeneous and distributed. As a result, compositional methods play an important role in the design and analysis of such complex systems. One such compositional analysis method is based on real-time calculus. In this paper, we present an analysis of fixed priority non-preemptive scheduling with the real-time calculus. Although fixed priority non-preemptive scheduling was modeled with the real-time calculus previously, we show that the model gives overly pessimistic results. We also compare our analysis with the existing holistic scheduling analysis through an example of a system using a controller area network (CAN) bus. The proposed method can be automated by incorporating it in the RTC toolbox.

Abstract Given deterministic interfacesPandQ, we investigate the problem of synthesising an interfaceRsuch thatPcomposed withRrefinesQ. We show that a solution exists iffPand are compatible, and the most general solution is given by , where is the interfacePwith inputs and outputs interchanged. Remarkably, the result holds both for asynchronous and synchronous interfaces. We model interfaces using the interface automata formalism of de Alfaro and Henzinger. For the synchronous case, we give a new definition of synchronous interface automata based on Mealy machines and show that the result holds for a weak form of nondeterminism, called observable nondeterminism. We also characterise solutions to the synthesis problem in terms of winning input strategies in the automaton , and the most general solution in terms of the most permissive winning strategy. We apply the solution to the synthesis of converters for mismatched protocols in both the asynchronous and synchronous domains. For the asynchronous case, this leads to automatic synthesis of converters for incompatible network protocols. In the synchronous case, we obtain automatic converters for mismatched intellectual property blocks in system-on-chip designs. The work reported here is based on earlier work on interface synthesis in Bhaduri (Third international symposium on automated technology for verification and analysis, ATVA 2005, pp 338–353, 2005) for the asynchronous case, and Bhaduri and Ramesh (Sixth international conference on application of concurrency to system design, ACSD 2006, pp 208–216) for the synchronous one.

Visual notations like class diagrams, and use case diagrams are very popular with practitioners for capturing requirements of software applications. These notations unfortunately have little or no semantics, and hence cannot be analyzed by tools. Formal notations, on the other hand, have associated tools that check specifications for stated properties but are difficult to integrate with software development processes in use. Strengths of both approaches can be exploited by giving formal semantics to popular notations. Here we propose a novel usage of UML object diagrams for specifying pre- and post-conditions for use cases and capturing global system properties as class invariants. A translation is defined from object diagrams to the formal notation TLA/sup +/. The TLA/sup +/ specification is then formally verified using the model checker TLC. The proposed notation is intuitive, expressive and formal. We present a small case study to illustrate its strengths.

Meta-model based development offers a promising way of managing the complexity of industrial scale software development by describing a system in terms of different 'views'. These views can then be described as instances of a single meta-model. Such views are usually not disjoint and it is essential that they are shown to be consistent. A weakness of meta-modelling tools is the lack of support for describing the behaviour of models, and this is central to demonstrating the consistency of views. We address this problem by combining meta-modelling with formal techniques for stating and verifying behavioural properties. In this paper, we describe a formalization of models and meta-models and show how this leads to automated procedures for consistency checking between views in an industrial software development framework.

This paper describes our experience in developing techniques for repairing date affected programs using standard compiler technology. Starting with date-ness information of certain variables based on their declarations, we propagate this information through all possible control paths, using date inference rules to traverse across individual statements. Our approach is fine grained enough to infer the date-ness of each occurrence of a variable. After detecting date-ness of variables, we renovate programs by applying a transformation using base year strategy. These techniques have been implemented as a tool set for renovating date affected COBOL programs. Copyright © 1999 John Wiley & Sons, Ltd.