Correct synchronisation in a distributed system is a difficult. One effective approach to the problem is to employ a logical clock on the high-level design, which ensures deterministic concurrency. However, most real-time network protocols only provide the means for physical time synchronisation. Therefore, in the end, the inherent logical clock has to be compiled away and mapped to physical time, losing many of its benefits. We propose a new middleware called softtide, which aims to facilitate the implementation and deployment of systems with an inherent logical clock. The idea is to provide a global logical clock through API, as the basis for scheduling task executions and message transmissions. At the same time, maintain a relatively stable relation between the logical clock and physical time, to limit the jitters between devices. The synchronisation mechanism is inspired by a recent protocol called bittide, which features a decentralised architecture. Softtide has the following mathematical properties: (1) Logical synchrony, where the transmission delays between devices are constant in logical time. (2) Its behaviour is deterministic even in the presence of network delays, differing clock frequencies, and faults. (3) Finally, softtide is decentralised in nature, where devices can dynamically join and leave. The synchronised logical clock provided by softtide simplifies the design, compilation, and validation of real-time distributed systems. Empirically we show the real-world performance of softtide to always produce deterministic results.

Correct synchronisation a distributed system is difficult. One effective approach to the problem is to employ a logical clock on the high-level design, which ensures deterministic concurrency. However, most real-time network protocols only provide physical time synchronisation. Therefore, in the end, the inherent logical clock has to be compiled away and mapped to physical time, losing many of its benefits.

We introduce Frequency Automata (FA), a new formal model that combines time and frequency domain representations. A sound translation from Hybrid Automata (HA) to FA is provided, along with a dedicated numerical simulator. Our method offers faster and more accurate simulation, especially in detecting level crossings. Experimental results show that FA outperforms Simulink/Stateflow®by up to 1129X in execution time and can handle equality guards that Simulink fails to detect.

Cyber-Physical Systems (CPSs), especially those involving autonomy, need guarantees of their safety. Runtime Enforcement (RE) is a lightweight method to formally ensure that some specified properties are satisfied over the executions of the system. Hence, there is recent interest in the RE of CPS. However, existing methods are not designed to tackle specifications suitable for the hybrid dynamics of CPS. With this in mind, we develop runtime enforcement of CPS using properties defined in Signal Temporal Logic (STL).

Machine Learning (ML) models are increasingly adopted in Cyber-Physical Systems (CPS), yet monolithic architectures hinder interpretability, verification, and safety assurance. By decomposing a CPS into modular sub-models and embedding formally defined safety policies during training, we can construct systems that are correct-by-construction rather than relying on post-hoc falsification or unscalable static verification.

Digital Twins (DTs) mimic a physical system using a digital version of the real system. While these have been explored in many domains, digital twins of human organs are yet to be created, especially those that are inspired by formal methods. To this end, we propose the first Cardiac Digital Twins (CDTs) by leveraging two key innovations from our research group.

Cryogenic power electronics has the potential to significantly improve Cyber Physical Systems (CPS) applications in aviation and space. However, their safety and reliability are yet to be studied systematically. To this end, we propose the first prototype of a deterministic toolchain for the design of Cryogenic Cyber Physical Systems (CCPS). Obviously, the design, verification and safety analysis of such systems pose considerable unknowns and challenges. Towards a potential solution, we propose an approach for unified functional safety, inspired by our earlier work. We leverage the recently developed deterministic framework (proposed by Google), called Logical Synchrony Networks, for distributed systems. This simplifies the modelling and safety analysis. Moreover, we propose a novel variant of Signal Temporal Logic (STL), called Synchronous Signal Temporal Logic (SSTL), which is specially tailored for CPS applications and designed using logical synchrony. We demonstrate the first prototype solution in the simulation of a CCPS system as a proof of concept.

As Industry 4.0 drives the Fourth Industrial Revolution, Cyber-Physical Systems (CPSs) have become central to industrial automation. These systems integrate software with physical processes, significantly improving the efficiency and adaptability. However, this integration also expands the attack surface, exposing systems to Cyber-Physical-attacks (CP-attacks) that can target either the computational components, physical devices, or both. The impact of such attacks can be catastrophic, ranging from system disruption to physical damage. Although numerous techniques have been developed to detect and mitigate these threats, industrial standards are often not incorporated into the design of these methods. This limits their deployment within the Industry 4.0 systems, where standard compliance is critical.

Massive strides in deterministic models have been made using synchronous languages. They are mainly focused on centralised applications, as the traditional approach is to compile away the concurrency. Time triggered languages such as Giotto and Lingua Franca are suitable for distribution albeit that they rely on physical clock synchronisation, which is both expensive and may suffer from scalability. Hence, deterministic programming of distributed systems remains challenging. We address the challenges of deterministic distribution by developing a novel multiclock semantics of synchronous programs. The developed semantics is amenable to seamless distribution. Moreover, our programming model, Timetide, alleviates the need for physical clock synchronisation by building on the recently proposed logical synchrony model for distributed systems. We discuss the important aspects of distributing computation, such as network communication delays, and explore the formal verification of Timetide programs. To the best of our knowledge, Timetide is the first multiclock synchronous language that is both amenable to distribution and formal verification without the need for physical clock synchronisation or clock gating.

Wearable and implantable medical devices (IMDs) are increasingly deployed to diagnose, monitor, and provide therapy for critical medical conditions. Such medical devices are safety-critical cyber-physical systems (CPSs). These systems support wireless features introducing potential security vulnerabilities. Although these devices undergo rigorous safety certification processes, runtime security attacks are inevitable. Based on published literature, IMDs such as pacemakers and insulin infusion systems can be remotely controlled to inject deadly electric shocks and excess insulin, posing a threat to a patient’s life. While prior works based on formal methods have been proposed to detect potential attack vectors using different forms of static analysis, these have limitations in preventing attacks at runtime. This article discusses a formal framework for detecting cyber-physical attacks on a pacemaker by monitoring its security policies at runtime. We propose a wearable device that senses the electrocardiogram (ECG) and photoplethysmogram (PPG) of the body to detect attacks in a pacemaker. To facilitate the design of this device, we map the security policies of a pacemaker w.r.t. ECG and PPG, paving the way for designing formal verification monitors for pacemakers for the first time using multiple physiological signals. The proposed monitoring framework allows the synthesis of parallel monitors from a given set of desired security policies, where all the monitors execute concurrently and generate an alarm to the user in the case of policy violation. Our implementation and the performance evaluation results demonstrate the technical feasibility of designing such a wearable device for attack detection in pacemakers. This device is separate from the pacemaker, ensuring no need for re-certification of pacemakers. Our approach is amenable to the application of security patches when new attack vectors are detected, making the approach ideal for runtime monitoring of medical CPSs.

A paradigm shift is underway in Software Engineering, with AI systems such as LLMs playing an increasingly important role in boosting software development productivity. This trend is anticipated to persist. In the next years, we expect a growing symbiotic partnership between human software developers and AI. The Software Engineering research community cannot afford to overlook this trend; we must address the key research challenges posed by the integration of AI into the software development process. In this article, we present our vision of the future of software development in an AI-driven world and explore the key challenges that our research community should address to realize this vision.

Real-time CPSs using Artificial Neural Networks (ANNs) are traditionally developed as monolithic black-boxes. This results in designs that are often difficult to formally verify against safety specifications and implement on hardware for formal timing analysis. Consequently, their implementation as a composition of smaller ANNs has received recent interest. These are easier to implement, parallelise and validate. Despite this, the question of how to produce hardware-implementable compositional designs from existing monolithic ones remains largely unanswered. This work develops a novel procedure to replace large ANN monolithic designs with smaller compositional designs and implement them on a Field Programmable Gate Array (FPGA) for timing analysis using synchronous compositional semantics. To illustrate our approach, we develop regression and classification ANN designs for multiple real-life datasets. Using various design and model architecture variations, we show that using a compositional design instead of a monolithic design can achieve an $\mathbf{8 5 \%}$ reduction in WCET, around a $\mathbf{53 \%}$ reduction in hardware resources and around a 40% reduction in computations and neuron connections for a minor reduction in performance.

Despite instructors' best efforts in designing and delivering any given course, changes are likely required from time to time. This experience report presents the changes made in a second-year programming course for non-computing engineering majors over a decade's worth of effort, and the reasons behind those changes. The changes were often reactive--in response to student feedback. However, many other changes were inspired by the desire to trial new interventions in the hope of strengthening the students' positive experience. In addition to personnel and course content changes, the gradual evolvement included how labs, assignments, and activities were structured and executed. Teaching delivery evolved, along with a number of small-scale interventions that eventually became integral elements of the course. When COVID-19 demanded a sudden shift to online learning, the course was prepared to adapt quickly and successfully. The contributions here come in the form of lessons learned over the past decade: what worked, and what did not. We present the large range of changes---and their rationales--that are particularly relevant and applicable to programming courses targeting engineering students where the luxury of pedagogically-friendlier programming languages is not possible.

Spiking Neural Networks (SNNs) have found increasing utility in designing safety-critical Cyber-Physical Systems (CPSs) such as implantable medical devices, autonomous vehicles, and space robotics due to their capability to operate on information represented in temporal coding and exhibit various behavioural modalities. Thus, there has been recent interest in formally verifying their timing behaviours and providing soundness guarantees of their diverse characteristics. However, beyond the simplistic Leaky Integrate and Fire (LIF) model, which only mimics 3 spiking behaviours, there is a lack of unifying methodology in literature to verify complex dynamics of biological neurons exhibiting 20 spiking behaviours as demonstrated by the pioneering work of Izhikevich. There is also a complete lack of formulation for the verification of SNN-based systems. This paper bridges these gaps by proposing a model-based approach for designing SNN-based controllers in CPS. We propose sound structural transformations translating any spiking neuron into networks of Timed Automata (TA), model the complex Izhikevich neural model and formally verify all 20 timing behaviours it exhibits for the first time. We then present two case studies that were modelled as SNNs using our approach: the PID controller, and the Car-Following controller, and subsequently attempt static model checking and statistical verification of their generated TA models for safety guarantees.

Embedded real-time systems are tightly integrated with their physical environment. Their correctness depends both on the outputs and timeliness of their computations. The increasing use of multi-core processors in such systems is pushing embedded programmers to be parallel programming experts. However, parallel programming is challenging because of the skills, experiences, and knowledge needed to avoid common parallel programming traps and pitfalls. This article proposes the ForeC synchronous multi-threaded programming language for the deterministic, parallel, and reactive programming of embedded multi-cores. The synchronous semantics of ForeC is designed to greatly simplify the understanding and debugging of parallel programs. ForeC ensures that ForeC programs can be compiled efficiently for parallel execution and be amenable to static timing analysis. ForeC’s main innovation is its shared variable semantics that provides thread isolation and deterministic thread communication. All ForeC programs are correct by construction and deadlock free because no non-deterministic constructs are needed. We have benchmarked our ForeC compiler with several medium-sized programs (e.g., a 2.274-line ForeC program with up to 26 threads and distributed on up to 10 cores, which was based on a 2.155-line non-multi-threaded C program). These benchmark programs show that ForeC can achieve better parallel performance than Esterel, a widely used imperative synchronous language for concurrent safety-critical systems, and is competitive in performance to OpenMP, a popular desktop solution for parallel programming (which implements classical multi-threading, hence is intrinsically non-deterministic). We also demonstrate that the worst-case execution time of ForeC programs can be estimated to a high degree of precision.

Diabetes is a global health threat, and its prevalence is rising at an alarming rate. Diabetes is the cause of severe complications in vital organs of the body. So, diabetes must be detected early for timely treatment and to prevent the condition from escalating to severe consequences. Many AI and machine learning approaches have been proposed for the non-invasive continuous monitoring of diabetes. However, using such informal methods in healthcare monitoring raises concerns about reliability. Furthermore, deploying an AI-based solution to continuously monitor a person's health state on resource-constrained embedded devices is a concern. We overcome these shortcomings in this work by proposing a formal runtime monitoring system for the first time for diabetes detection using Electrocardiogram (ECG) sensing. We implement a data mining model from the ECG features to infer ECG policies and thereby synthesize a formal verification monitor based on the policies. Using a diabetes dataset, we evaluate the verification monitor's performance compared to other proposed models.

Automatic detection of cardiac arrhythmia is an important tool in the fight against cardiovascular diseases and their associated human impacts. Such detection needs to be both accurate and timely, in order to allow for interventions to be administered within short time frames. Traditionally, such approaches have used black box implementations which are not explainable and hence have limited use in terms of clinical interpretability. Additionally, these implementations may either require additional training between patients, or have processing times which make them unsuitable for real-time classification. To address this, we develop a set of formal Timed Automaton-based policies that capture three common arrhythmia, Premature Ventricular Contraction, Ventricular Tachycardia, and Atrial Fibrilation, in terms of Electrocardiogram (ECG) features. We synthesise Runtime Verification monitors for each of these policies, and run them alongside existing clinical ECG databases to evaluate their efficacy. This approach shows comparable results to existing black box work with accuracies ranging from 90 % to 96 % while still being both explainable and clinically interpretable.

Unmanned aerial drones are Cyber-Physical Systems (CPSs) with increasing availability, popularity, and capability. Although other aeronautical and safety-critical industries apply stringent regulations and design approaches, smaller drones tend to have much weaker and informal design requirements. Due to the strong open-source movement in this space, there are numerous opportunities for malicious actors to find weaknesses to attack drone systems, and in parallel develop their own rogue drones. These factors present a risk of damage to people and property in addition to compromise of integrity and availability. However, a formal framework for ethical hacking that combines attacker modelling and launching of attacks is lacking in the literature. To this end, we leverage runtime enforcement, combined with the idea of suspension from synchronous programming to develop the first such formal framework. The proposed framework enables the modelling of complex attack vectors on drones. To facilitate this, we propose a bespoke policy-based runtime enforcement framework called enforcer interchange (EI). It is capable of both individual intent/target-specific attacks as well as more sophisticated combinations of attacks, which it manages by enabling and disabling attack enforcers at runtime in a context-aware manner. To demonstrate our framework, we utilise a quadcopter drone simulator and record the changes in the drone's behaviour as it executes a range of missions under different attacks. Our approach provides a framework for testing drones' resilience and defenses against malicious attacks, as well as exploring the capabilities of rogue drones.

Model based design of embedded controllers is prevalent across different industries. The final step in model based design is synthesis of hardware (or software) controller and then testing the synthesized controller in closed-loop with the plant model - this is termed as co-simulation. Standard cosimulation approaches use asynchronous communication fabric. However, they are known to suffer from race conditions, jitter, etc, making real-time property validation difficult. Current approaches to co-simulation problems either require complex middle-ware or require synthesis of the controller and plant for synchronous execution. However, these approaches are unsuited for hybrid system control design and validation, as they require the plant model to execute at an arbitrarily small simulation step, while the synthesized controller executes at its own rate if any. The small simulation step slows down the simulation and such a setup does not guarantee level crossing detection. In this paper, we propose a novel Metric Interval Temporal Logic (MITL) based validation and Hardware in Loop (HIL) co-simulation framework, which synchronizes and integrates the controller synthesized in hardware and the plant executing in software. A discrete controller handles a level crossing generated by the plant, which evolves on variable step size. The traces generated from the closed-loop operation of the overall system are used to validate MITL properties. Finally, the controller hardware and the plant model are adjoined via a communication architecture, whose sample time is dependent upon the robustness estimates of the MITL properties, which is necessary to guarantee validation correctness.

Worst Case Execution Time (WCET) analysis of large and complex hybrid systems can be time consuming. Contract based design allows for compositional reasoning of complex systems. Contracts justify the behavior of a system by way of assumptions (which are to be satisfied by the system environment) and guarantees, which are to be met by the system. Contracts also play a major role in compositional reasoning, refinement and re-usability of the system components. In this paper, we present a formal framework to enforce real-time contracts using Hoare triples, for synchronous system design and verification. In that regard, we propose real-time Hoare rules which are based on the WCET of the system and its components. We verify the real-time behavior of the system by applying these rules. These rules not only justify the system behavior and the behavior of its components but their timing as well. We also show that these Hoare rules are sound. Then we show that the synchronous composition of component level Hoare rules based contracts justify a system level contract. This real-time contract composition and reasoning technique which is based on real-time Hoare logic rules is the first ever attempt in synchronous system design and verification.

Hybrid systems are a subset of Cyber-Physical System (CPS), where a physical process (the plant) is controlled by a discrete controller. The controller induces mode switches, which are modelled as guard conditions leading to sudden discontinuities. Correctly capturing sudden discontinuities during simulation is the primary challenge to maintain fidelity. De-facto industry standard tools, such as Simulink and Modelica, have been known to produce incorrect outputs when simulating systems involving complicated guards. For example, transcendental guards leading to the well-known even number of level crossing detection problem or guards leading the system state into the complex plane have been shown to produce invalid results. To tackle this problem we propose Higher Order Hybrid Automata and its compositional execution semantics. Using this semantics a novel numerical simulation approach for hybrid systems is developed. The key idea is to approximate the guard and Ordinary Differential Equations with Taylor polynomials so as to accurately detect zero-crossings induced by the guards. Simulation results show that systems with transcendental guards can be simulated using our approach efficiently, while maintaining high simulation fidelity.

IEEE 1588 is a time synchronization protocol that is extensively used by many Cyber-Physical Systems (CPSs). However, this protocol is prone to various types of attacks. We focus on a specific type of Man-in-the-Middle (MITM) attack, where the attacker introduces random delays to the messages being exchanged between a master and a slave. Such attacks have been modelled previously and some mitigation strategies have also been developed. However, the proposed methods work only under constant delay attacks and the developed mitigation strategies are ad-hoc. We propose the first formal framework for modelling and mitigating time delay attacks in IEEE 1588. Initially, the master, the slave and the communication medium are modelled as Timed Automata (TA) assuming the absence of any attacks. Subsequently, a generic attacker is modelled as a TA, which can formally represent various attacks including constant delay, linear delay and exponential delay. Finally, system identification methods of control theory is used to design proportional controllers for mitigating the effects of time delay attacks. We use model checking to ensure the resilience of protocol to time delay attacks using the proposed mitigation strategy.

Wearable and implantable medical devices are being increasingly deployed for diagnosis, monitoring, and to provide therapy for critical medical conditions. Such medical devices are examples of safety-critical, cyber-physical systems. In this paper we focus on insulin infusion systems (IISs), which are used by diabetics to maintain safe blood glucose levels. These systems support wireless features introducing potential vulnerabilities. Although these devices go through rigorous safety certification processes, these are not able to mitigate security threats. Based on published literature, attackers can remotely command to inject an incorrect amount of insulin thereby posing threat to a patient's life. While prior work based on formal methods have been proposed to detect potential attack vectors using different forms of static analysis, these have limitations in preventing attacks at run-time. Also, as these devices are safety critical, it is not possible to apply security patches, when new types of attacks are detected, due to the need for recertification.

Rear-end collision avoidance relies on mathematical models to calculate the safety distance. Vehicle deceleration is a key parameter for the accuracy of the models. Current models, however, assume a constant deceleration during braking, which is unrealistic. This assumption results in large over-approximation / under-approximation. In this paper, we rectify this limitation by proposing a new model that accounts for realistic vehicle deceleration during braking. Simulation results show that our approach guarantees safety. Moreover, traffic flow is improved by 21.6% compared to the widely adopted the Berkeley algorithm.

Real-time systems are designed using model-driven approaches, where a complex system is represented as a set of interacting components. Such a compositional approach facilitates design of simpler components, which are easier to validate and integrate with the overall system. In contrast to such systems, data-driven systems like neural networks are designed as monolithic black-boxes to capture the non-linear relationship from inputs to outputs. Increasingly, such systems are being used in safety-critical real-time systems. Here, a compositional approach would be ideal. However, to the best of our knowledge, such a compositional approach is lacking while designing data-driven components based on neural networks.This paper formalises this problem by developing the concept of Composed Neural Networks (CpNNs) by extending the well known Keras python framework. CpNNs formalise the synchronous composition of several interacting neural networks in Keras. Further, using the developed semantics, we enable modular compilation from a given CpNN to C code. The generated code is suitable for the Worst-Case Execution Time (WCET) analysis. Using several benchmarks we demonstrate the superiority of the developed approach over a recently proposed approach using Esterel, as well as the popular Python package Tensorflow Lite. For the given benchmarks, our approach is superior to Esterel with an average WCET reduction of 64.06%, and superior to Tensorflow Lite with an average measured WCET reduction of 62.08%.

Cardiovascular Implantable Electronic Devices (CIEDs) are routinely implanted to treat various types of arrhythmia. However, conventional pacing algorithms may not be able to provide optimal treatment for the patients with Heart Failure (HF) and evidence suggests negative outcomes. In this paper, we introduce a formal pacemaker model that can restore heart-lung synchronization, which may bring therapeutic benefits to the patient with chronic HF. We use valued Synchronous Discrete Timed Automata (SDTA) to describe the timing requirements of the device, which is then translated into Promela for formal verification through a set of rules which are defined to maintain the synchronous semantics. The safety-critical properties are then verified using the model checker SPIN. We show that the SDTA model can be verified more efficiently than conventional approaches with pure Timed Automata (TA). Animal test results show that the pacing rates are synchronized with the respiratory cycles. In particular, the functional safety is ensured under various respiratory conditions. This work yields, for the first time, a formal model of pacing device to reinstate heart rate variability for HF patients.

Co-simulation--based validation of hardware controllers adjoined with plant models, with continuous dynamics, is an important step in model-based design of controllers for Cyber-physical Systems (CPS). Co-simulation suffers from many problems, such as timing delays, skew, race conditions, and so on, making it unsuitable for checking timing properties of CPS. In our approach to validation of controllers, synthesised from their models, the synthesised controller is adjoined with a synthesised hardware plant unit. The synthesised plant and controller are then executed synchronously and Metric Interval Temporal Logic (MITL) properties are validated on the closed-loop system. The clock period is chosen, using robustness estimates, such that all timing properties that hold on the controller guiding the discretised plant model also hold on the original case of the continuous-time plant model guided by the controller. Benchmark results show that real-time MITL properties that are vacuously satisfied or violated due to co-simulation artefacts hold correctly in the proposed closed-loop validation framework.

Cyber-physical systems (CPSs) are implemented in many industrial and embedded control applications. Where these systems are safety-critical, correct and safe behavior is of paramount importance. Malicious attacks on such CPSs can have far-reaching repercussions. For instance, if elements of a power grid behave erratically, physical damage and loss of life could occur. Currently, there is a trend toward increased complexity and connectivity of CPS. However, as this occurs, the potential attack vectors for these systems grow in number, increasing the risk that a given controller might become compromised. In this article, we examine how the dangers of compromised controllers can be mitigated. We propose a novel application of runtime enforcement that can secure the safety of real-world physical systems. Here, we synthesize enforcers to a new hardware architecture within programmable logic controller I/O modules to act as an effective line of defence between the cyber and the physical domains. Our enforcers prevent the physical damage that a compromised control system might be able to perform. To demonstrate the efficacy of our approach, we present several benchmarks, and show that the overhead for each system is extremely minimal.

OBJECTIVE: Cardiovascular Implantable Electronic Devices (CIEDs) are used extensively for treating life-threatening conditions such as bradycardia, atrioventricular block and heart failure. The complicated heterogeneous physical dynamics of patients provide distinct challenges to device development and validation. We address this problem by proposing a device testing framework within the in-silico closed-loop context of patient physiology. METHODS: We develop an automated framework to validate CIEDs in closed-loop with a high-level physiologically based computational heart model. The framework includes test generation, execution and evaluation, which automatically guides an integrated stochastic optimization algorithm for exploration of physiological conditions. CONCLUSION: The results show that using a closed loop device-heart model framework can achieve high system test coverage, while the heart model provides clinically relevant responses. The simulated findings of pacemaker mediated tachycardia risk evaluation agree well with the clinical observations. Furthermore, we illustrate how device programming parameter selection affects the treatment efficacy for specific physiological conditions. SIGNIFICANCE: This work demonstrates that incorporating model based closed-loop testing of CIEDs into their design provides important indications of safety and efficacy under constrained physiological conditions.

Cyber-Physical Systems are highly safety critical, especially since they have to provide both functional and timing guarantees. Increasingly, Cyber-Physical Systems such as autonomous vehicles are relying on Artificial Neural Networks in their decision making and this has obvious safety implications. While many formal approaches have been recently developed for ensuring functional correctness of machine learning modules involving Artificial Neural Networks, the issue of timing correctness has received scant attention.

In recent years we have seen numerous proof-of-concept attacks on implantable medical devices such as pacemakers. Attackers aim to breach the strict operational constraints that these devices operate within, with the end-goal of compromising patient safety and health. Most efforts to prevent these kinds of attacks are informal, and focus on application- and system-level security --- for instance, using encrypted communications and digital certificates for program verification. However, these approaches will struggle to prevent all classes of attacks. Runtime verification has been proposed as a formal methodology for monitoring the status of implantable medical devices. Here, if an attack is detected a warning is generated. This leaves open the risk that the attack can succeed before intervention can occur. In this paper, we propose a runtime-enforcement based approach for ensuring patient security. Custom hardware is constructed for individual patients to ensure a safe minimum quality of service at all times. To ensure correctness we formally verify the hardware using a model-checker. We present our approach through a pacemaker case study and demonstrate that it incurs minimal overhead in terms of execution time and power consumption.

Simulink/Stateflow® is the de-facto tool for design of Cyber-physical Systems (CPS). CPS include hybrid systems, where a discrete controller guides a continuous plant. Hybrid systems are characterised by their continuous time dynamics with sudden discontinuities, caused by level/zero crossings. Stateflow can graphically capture hybrid phenomenon, making it popular with control engineers. However, Stateflow is unable to correctly and efficiently simulate complex hybrid systems, especially those characterised by even number of level crossings.

The emerging Die-stacking technology enables DRAM to be used as a cache to break the “Memory Wall” problem. Recent studies have proposed to use DRAM as a victim cache in both CPU and GPU memory hierarchies to improve performance. DRAM caches are large in size and, hence, when realized as a victim cache, non-inclusive design is preferred. This non-inclusive design adds significant differences to the conventional DRAM cache design in terms of its probe, fill, and writeback policies. Design and verification of a victim DRAM cache can be much more complex than that of a conventional DRAM cache. Hence, without rigorous modeling and formal verification, ensuring the correctness of such a system can be difficult. The major focus of this work is to show how formal modeling is applied to design and verify a victim DRAM cache. In this approach, we identify the agents in the victim DRAM cache design and model them in terms of interacting state machines. We derive a set of properties from the specifications of a victim cache and encode them using Linear Temporal Logic. The properties are then proven using symbolic and bounded model checking. Finally, we discuss how these properties are related to the dataflow paths in a victim DRAM cache.

Synchronous Programming ( SP ) is a universal computational principle that provides deterministic concurrency. The same input sequence with the same timing always results in the same externally observable output sequence, even if the internal behaviour generates uncertainty in the scheduling of concurrent memory accesses. Consequently, SP languages have always been strongly founded on mathematical semantics that support formal program analysis. So far, however, communication has been constrained to a set of primitive clock-synchronised shared memory ( csm ) data types, such as data-flow registers, streams and signals with restricted read and write accesses that limit modularity and behavioural abstractions. This paper proposes an extension to the SP theory which retains the advantages of deterministic concurrency, but allows communication to occur at higher levels of abstraction than currently supported by SP data types. Our approach is as follows. To avoid data races, each csm type publishes a policy interface for specifying the admissibility and precedence of its access methods. Each instance of the csm type has to be policy-coherent, meaning it must behave deterministically under its own policy—a natural requirement if the goal is to build deterministic systems that use these types. In a policy-constructive system, all access methods can be scheduled in a policy-conformant way for all the types without deadlocking. In this paper, we show that a policy-constructive program exhibits deterministic concurrency in the sense that all policy-conformant interleavings produce the same input-output behaviour. Policies are conservative and support the csm types existing in current SP languages. Technically, we introduce a kernel SP language that uses arbitrary policy-driven csm types. A big-step fixed-point semantics for this language is developed for which we prove determinism and termination of constructive programs.

Existing techniques for validation of implantable medical devices such as pacemakers are heavily dependent on expensive and timeconsuming clinical trials where the sample size is small and may not represent the variance in a larger population. To address this problem, bio-engineering researchers have proposed various high fidelity models that are used for non real-time simulation. More recently, computer science (CS) researchers have developed more abstract models that are amenable for real-time (hardware-in-the loop validation), but fail to exhibit appropriate dynamic responses. In general, the challenge remains on how to develop the organ models such that they capture the appropriate behaviour while maintaining the real-time response. In this paper, we present a generic step-by-step methodology that can aid researchers who are modelling organs for the validation of medical devices. The goal of this paper is to help: (1) introduce CS researchers to the steps involved in extracting executable organ models from bio-engineering models (2) introduce bio-engineers to emulation models and available computer hardware platforms for synthesising the organ models.

In industrial automation, safety-critical control systems need robust timing guarantees in addition to functional correctness. Unfortunately, devices that are typically used in this domain, such as Programmable Logic Controllers, often feature architectures that are not amenable to static timing analysis, for instance relying on general purpose microprocessors or embedded operating systems. As a result, designers often rely on timing values gained from simple measurement of running applications, an approach that only provides very weak guarantees at best. The synchronous approach for IEC 61499 Function Blocks, in contrast, has been demonstrated to be time predictable when run on appropriate hardware, such as simple microprocessors. However, simple microprocessors are often not fast or powerful enough for modern automation requirements. In this paper, we examine how the performance of synchronous IEC 61499 can be improved through the usage of the multi-core T-CREST architecture, data scratchpads, and an optimised compiler. Overall, our improvements resulted in 60% shorter worst-case execution times.

The US Food and Drug Administration (FDA) recently recalled approximately 465,000 pacemakers that were vulnerable to hacking. It was reported that hackers could either pace the devices rapidly inducing arrhythmia or could drain the battery. Such actions would compromise the health and well being of the patient concerned. Considering this, techniques to ensure the security of implantable medical devices is an emerging area of research. To the best of our knowledge, existing techniques lack the formal rigour for ensuring the safety and security of such systems. While methods exist for formal verification of pacemaker software, these are not suitable to prevent security vulnerabilities. To this end we develop a run-time verification based approach. Our approach proposes a wearable device that non-invasively senses the familiar ECG signals in order to determine if a pacemaker has been compromised. We develop a set of timed policies to be monitored at run-time. We provide a methodology for the design of the wearable device and results demonstrate the technical feasibility of the developed concept.

Cyber-physical systems (CPS), such as autonomous vehicles or smart power grids, use interactive machine learning modules for decision making. Current design approaches use multiple machine learning modules, often using neural networks, to achieve the desired functionality. Timing validation is performed using measurement-based approaches, which may produce unsound results. To this end, we propose a new approach for designing such systems, by relying on the well known synchronous paradigm. Using this approach, we introduce Synchronous Artificial Neural Networks (SANNs), where we associate logical time to the different operations of the network. This approach provides sound compositional primitives, which enable the composition of interacting neural networks to ensure causality and determinism. We then show that we can embed the generated code on time predictable platforms enabling static analysis. Overall, this paper develops synchronous neural networks implemented in Esterel for the design of time predictable systems. We demonstrate the efficacy of our approach by developing a time predictable implementation of several applications, ranging from 5-100+ neurons, realised using the T-CREST platform. We also implemented a complex Convolutional Neural Network (CNN) application comprising of 1000+ neurons and 16 different layers using Esterel for a soft real-time application. Overall, the developed methodology opens new avenues of research in the direction of time predictable neural networks.

Die-stacking technology enables the use of a high density DRAM as a cache. Major processor vendors have recently started using these stacked DRAM modules as the last level cache of their products. These stacked DRAM modules provide high bandwidth with relatively low latency compared to the off-package DRAM modules. Recent studies on DRAM caches propose several variants to optimize performance and power of the systems. However, none of the existing works discuss its design and verification aspect. DRAM cache controller (DCC) design is significantly complex in comparison to a conventional DRAM-based main memory controller. This is because it involves controlling both the timing aspect of DRAM system as well as the functional aspect of cache. Therefore, without rigorous modeling and verification of such designs, it would be difficult to ensure correctness. In the current research, we focus on the design and verification issues of DCC. We select a common variant of DRAM cache and build a formal model of its controller in terms of interacting state machines; we term the common variant as the baseline and its model as the base model. We then verify safety, liveness, and timing properties of this variant using model checking. Next, we demonstrate how the formal models and the associated properties of other variants of DCCs can be derived from the base model in a systematic way. Analyzing the individual DRAM cache variations, we observe that most of the variants exhibit product-line characteristics.

The heart is a vital organ that relies on the orchestrated propagation of electrical stimuli to coordinate each heartbeat. Abnormalities in the heart’s electrical behaviour can be managed with a cardiac pacemaker. Recently, the closed-loop testing of pacemakers with an emulation (real-time simulation) of the heart has been proposed. This enables developers to interrogate their pacemaker design without having to engage in costly or lengthy clinical trials. Many high-fidelity heart models have been developed, but are too computationally intensive to be simulated in real-time. Heart models, designed specifically for the closed-loop testing of pacemaker logic, are too abstract to be useful for the testing of pacemaker implementations. In the context of pacemaker testing, compared to high-fidelity heart models, this article presents a more computationally efficient heart model that generates realistic piecewise continuous electrical signals. The heart model is composed of cardiac cells that are connected by paths. Our heart model is based on the Stony Brook cardiac cell model and the UPenn path model, and improves them by stabilising the activation behaviour of the cells and by capturing the piecewise continuous behaviour of electrical propagation. We provide simulation results that show our ability to faithfully model a range of arrhythmias, such as VA conduction, heart blocks, and long Q-T syndrome. Moreover, re-entrant circuits (that cause arrhythmia) can be faithfully modelled, which only the discrete-event UPenn heart model is also able to achieve.

Automation systems used in smart grids, transportation, and medical electronics are cyber physical in nature. Automation standards, such as IEC-61499, while well suited to the design of discrete controllers, are not ideally suited to model the dynamics of the plant. Such modeling is essential for emulation-based validation of the controllers in the cyber-physical systems (CPS) domain. We use a well-known formal model for CPS, called hybrid input output automata (HIOA), as the main vehicle in the proposed formulation. A physical process (the plant) may be described as a synchronous composition of a network of such HIOA. We provide an approach to transform such a network to a composite function block (CFB) in IEC-61499. This transformation is shown to be semantics preserving. Code generated from such plant models can be executed on a computer chip to provide real-time response to their adjoining controllers. Through practical examples, we illustrate the scalability and practicability of the proposed approach. The developed approach enables the emulation of physical processes in industrial automation without using the actual plant.

Car-following is the activity of safely driving behind a leading vehicle. Traditional mathematical car-following models capture vehicle dynamics without considering human factors, such as driver distraction and the reaction delay. Consequently, the resultant model produces overly safe driving traces during simulation, which are unrealistic. Some recent work incorporate simplistic human factors, though model validation using experimental data is lacking. In this paper, we incorporate three distinct human factors in new compositional car-following model called modal car-following model, which is based on hybrid input output automata (HIOA). HIOA have been widely used for the specification and verification of cyber-physical systems. HIOA incorporate the modeling of the physical system combined with discrete mode switches, which is ideal for describing piece-wise continuous phenomena. Thus, HIOA models offer a succinct framework for the specification of car-following behavior. The human factors considered in our approach are estimation error (due to imperfect distance perception), reaction delay, and temporal anticipation. Two widely used car-following models called Intelligent Driver Model (IDM) and Full Velocity Difference Model (FVDM) are used for extension and comparison purpose. We evaluate the root mean square (rms) error of the following vehicle position using the traces obtained from human drives through different driving scenarios. The result shows that our model reduces the rms error in IDM and FVDM by up to 48.8% and 7.41%, respectively.

Sensitive (private) information can escape from one app to another using one of the multiple communication methods provided by Android for inter-app communication. This leakage can be malicious. In such a scenario, individual benign app, in collusion with other conspiring apps, if present, can leak the private information. In this work in progress, we present, a new model-checking based approach for inter-app collusion detection. The proposed technique takes into account simultaneous analysis of multiple apps. We are able to identify any set of conspiring apps involved in the collusion. To evaluate the efficacy of our tool, we developed Android apps that exhibit collusion through inter-app communication. Eight demonstrative sets of apps have been contributed to widely used test dataset named DroidBench. Our experiments show that proposed technique can accurately detect the presence/absence of collusion among apps. To the best of our knowledge, our proposal has improved detection capability than other techniques.

In this paper we propose a WCRT analysis technique for synchronous programs, executed as sequential or multi-threaded code, based on formal power series in min-max-plus algebra. The algebraic model constitutes the first fully declarative timing-aware semantics of synchronous programs with arbitrary hierarchical control-flow structure. Under signal abstraction this model permits efficient compositional WCRT analyses based on structural boxes as the unit of composition. The algebraic model leads to a sound methodology to deal with the state space explosion arising from tick alignment of parallel composition by reduction to the maximum weighted clique problem.

Implantable medical devices such as cardiac pacemakers have been recalled frequently with safety related issues. This paper proposes a model driven approach for pacemaker design by combining the strengths of two well-known philosophies for safety critical systems. First, we adopt the SCCharts synchronous language for pacemaker specification. Second, we adopt a PRET architecture for the underlying processor which has been modified to include reactive semantics. PRET processors offer an ideal platform for providing timing guarantees. We use automatic code generation combined with static timing analysis during the design phase. Also, we use an existing emulation model of the human heart using a 33-node conduction network for closed loop validation of the designed pacemaker.

IEC61499 is an emerging standard for the design of automation systems. While many compilers and associated tools for IEC61499 have been developed, systematic techniques for modelling the continuous dynamics of the physical processes are lacking. Current practices involve using co-simulation, where plants are modelled in a tool such as Simulink and controllers are designed using IEC-61499. Co-simulation has many limitations such as slow sampling and free-wheeling. In this paper we propose a systematic approach for the design and simulation of Cyber-Physical Systems (CPS) using IEC61499. We propose the concept of Hybrid Function Blocks (HFBs), as syntactic extensions, to specify the continuous dynamics of a physical plant. A Hybrid Function Block can be compiled into a standards compliant Basic Function Block, based on new deterministic synchronous semantics. To show that our approach is both scalable and efficient when designing CPS, we present benchmarks showing that it runs 29 % faster than Simulink when generating correlating traces.

Synchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem of runtime enforcement in the context of synchronous programs. We propose a framework where an enforcer monitors both the inputs and the outputs of a synchronous program and (minimally) edits erroneous inputs/outputs in order to guarantee that a given property holds. We define enforceability conditions, develop an online enforcement algorithm, and prove its correctness. We also report on an implementation of the algorithm on top of the KIELER framework for the SCCharts synchronous language. Experimental results show that enforcement has minimal execution time overhead, which decreases proportionally with larger benchmarks.

Models of the cardiac conduction system are usually at two extremes: (1) high fidelity models with excellent precision but lacking a real-time response for emulation (hardware in the loop simulation); or (2) models amenable for emulation, but that do not exhibit appropriate dynamic response, which is necessary for arrhythmia susceptibility. We introduce two abstractions to remedy the situation. The first abstraction is a new cell model, which is a semi-linear hybrid automata. The proposed model is as computationally efficient as current state-of-the-art cell models amenable for emulation. Yet, unlike these models, it is also able to capture the dynamic response of the cardiac cell like the higher-fidelity models. The second abstraction is the use of smooth-tokens to develop a new path model, connecting cells, which is efficient in terms of memory consumption. Moreover, the memory requirements of the path model can be statically bounded and are invariant to the emulation step size. Results show that the proposed semi-linear abstraction for the cell reduces the execution time by up to 44%. Furthermore, the smooth-tokens based path model reduces the memory consumption by 40 times when compared to existing path models. This paves the way for the emulation of complex cardiac conduction systems, using hardware code-generators.

Hybrid systems combine discrete controllers with adjoining physical processes. While many approaches exist for simulating hybrid systems, there are few approaches for their emulation, especially when the actual physical plant is not available. This paper develops the first formal framework for emulation along with a new compiler that enables large-scale (1000+ components) simulation. We propose a formal model called Synchronous Emulation Automaton (SEA) specifically for modular compilation and parallel execution. SEA combines Linear Time Invariant (LTI) systems with discrete mode switches and has the following semantic differences with Hybrid Automata: ➀ the Ordinary Differential Equations are solved analytically and the solutions are sampled at the Worst-Case Reaction Time of the model and ➁ we develop a new composition semantics, which allows individual SEAs to execute in parallel with each other. The proposed semantics eliminates: ⓐ the need for dynamic numerical solvers, and ⓑ the Zeno-phenomenon by construction. Experimental results show that process models designed using our tool (Piha) give a 3.6 times execution speedup over Simulink®, and upto 26 times speedup on manycore architectures.

Many implantable medical devices, such as pacemakers, have been recalled due to failure of their embedded software. This motivates rethinking their design and certification processes. We propose, for the first time, an additional layer of safety by formalising the problem of run-time enforcement of implantable pacemakers. While recent work has formalised run-time enforcement of reactive systems, the proposed framework generalises existing work along the following directions: (1) we develop bi-directional enforcement, where the enforced policies depend not only on the status of the pacemaker (the controller) but also of the heart (the plant), thus formalising the run-time enforcement problem for cyber-physical systems (2) we express policies using a variant of discrete timed automata (DTA), which can cover all regular properties unlike earlier frameworks limited to safety properties, (3) we are able to ensure the timing safety of implantable devices through the proposed enforcement, and (4) we show that the DTA-based approach is efficient relative to its dense time variant while ensuring that the discretisation error is relatively small and bounded. The developed approach is validated through a prototype system implemented using the open source KIELER framework. The experiments show that the framework incurs minimal runtime overhead.

Synchronous languages are ideal for designing safety-critical systems. Static Worst-Case Reaction Time (WCRT) analysis is an essential component in the design flow that ensures the real-time requirements are met. There are a few approaches for WCRT analysis, and the most versatile of all is explicit path enumeration. However, as synchronous programs are highly concurrent, techniques based on this approach, such as model checking, suffer from state explosion as the number of threads increases. One observation on this problem is that these existing techniques analyse the program by enumerating a functionally equivalent automaton while WCRT is a non-functional property. This mismatch potentially causes algorithm-induced state explosion. In this paper, we propose a WCRT analysis technique based on the notion of timing equivalence, expressed using WCRT algebra. WCRT algebra can effectively capture the timing behaviour of a synchronous program by converting its intermediate representation Timed Concurrent Control Flow Graph (TCCFG) into a Tick Cost Automaton (TCA), a minimal automaton that is timing equivalent to the original program. Then the WCRT is computed over the TCA. We have implemented our approach and benchmarked it against state-of-the-art WCRT analysis techniques. The results show that the WCRT algebra is 3.5 times faster on average than the fastest published technique.

The IEC 61499 standard enables the model-based design of complex industrial automation systems, in which a model of the controlled physical processes called a plant, is codeveloped with the controller. However, the existing design flow does not address functional safety issues, which include limiting risk to acceptable levels. Standards like IEC 61508 provide safety guidelines for measuring and managing risk to acceptable ranges using quantitative or probabilistic methods for hardware, and qualitative or systematic analysis techniques for software. Such analyses are inadequate in situations where safety depends on both hardware and software. This paper proposes a unifying model-based approach for the quantitative and qualitative analysis of IEC 61499 designs. The approach combines Markov analysis and model checking to estimate quantified risk and is more expressive than traditional analyses like reliability block diagrams. At design level, unified safety requirements are captured using safety blocks, which is an extension of the IEC 61499 basic blocks. The PRISM model checker is used to analyze the system, based on a sound conversion of IEC 61499 designs into PRISM models. A tool-chain enabling the proposed approach shows encouraging benchmarking results confirming the feasibility of unified analysis.

The synchronous paradigm is widely used for the design of safety critical systems. Such systems, especially in the medical devices domain, must meet strict timing requirements while also ensuring long battery life. As a consequence, they are subject to very strict constraint both regarding their WCRT (Worst-Case Reaction Time) and their WCEC (Worst-Case Energy Consumption, the equivalent constraint for the energy consumption). Many techniques exist to compute an upper bound on the WCRT, but few techniques exist that address both the WCRT and the WCEC. We propose here a static analysis framework where conventional WCRT analysis interacts with a DVFS (Dynamic Voltage Frequency Scaling) algorithm to minimize also the WCEC of the given synchronous program. Our algorithm is able to compute the Pareto front of non-dominated solutions in the (WCRT, WCEC) space. Experimental results reveal that the proposed approach is scalable in terms of analysis time while providing more non-dominated solutions compared to two existing approaches. To the best of our knowledge, the proposed approach is the first to produce energy and timing aware synchronous programs.

Mixed-Criticality Systems are capable of accommodating tasks of varying criticality. In this paper, these are [life, mission, and non-critical]. Tasks usually have an overestimated execution time to allow for the Worst Case Execution Time (WCET). When these tasks finish execution prior to their allotted execution time due to pessimistic assumptions present in the static analysis of the system. The surplus time is used to accommodate tasks with tolerance for deadline-misses. Non-critical tasks are often treated in a ”best-effort” capacity where no quality of service is considered. When processor utilisation is not overconstrained, all deadlines will be met. However, in cases where not enough processing resources exist to meet all deadlines for non-critical tasks, the allotted time for the non-critical tasks must be rationed between non-critical tasks. This paper proposes a novel method of prioritising non-critical tasks. By treating task execution as a service, non-critical tasks with unbounded deadline miss tolerance are given a Grade of Service for their met deadlines. This Grade of Service is used for the dynamic scheduling of non-critical tasks. Four different scheduling algorithms were tested with the proposed Highest Penalty First algorithm for distributing the effort of task execution amongst non-critical tasks in a proportionate manner and showing superior fairness of task execution compared to all other tested algorithms.

Many complex industrial control systems need to meet stringent timing requirements. Ensuring that implementations can meet these requirements can be a very difficult task. IEC 61499 is an emerging standard for modelling and implementing large distributed industrial control systems. However, there is currently no established approach for executing IEC 61499 code in a distributed time-predictable manner. In this paper, we present a novel time-predictable runtime called RunSync for executing IEC 61499 on the Precision Timed (PRET) architecture FlexPRET. PRET architectures are designed to guarantee timing repeatability while preserving performance. They are often designed as RISC architectures which utilize multiple hardware threads to remove pipeline hazards. Determining the allocation of tasks to the hardware threads is a key problem when utilizing such architectures. Hence, in this paper it is demonstrated that through RunSync it is possible to dynamically map IEC 61499 tasks to hardware threads during runtime, while preserving determinism and remaining amenable to timing analysis. Following that, quantitative results are presented, showing the minimal overheads of RunSync compared to implementations of the existing synchronous approach. RunSync is thus demonstrated to be more performant with large IEC 61499 networks, and when there are more hardware resources to be allocated.

IEC 61499 enables component-oriented descriptions of complex industrial processes facilitating model-driven engineering. One aspect that is lacking, however, is the ability to directly express Statecharts-like hierarchy and concurrency within basic function blocks (BFBs). Such features can significantly enhance function blocks and help create more succinct and readable specifications. We propose a new syntactic extension to the standard called hierarchical and concurrent execution control chart (HCECC). A major roadblock for any suggested changes to the standard is the need for compliance. Our approach extends the synchronous execution semantics of IEC 61499, where HCECCs are purely syntactic sugar. Using a revised synchronous semantics, our compiler generates standard compliant C code from HCECCs. Benchmarking and usability studies reveal the relative superiority of the proposed approach over existing approaches.

Transmission timing and delay between communicating vehicles are two important performance measures for safety-critical applications of Vehicular Ad-Hoc Networks (VANETS). Safety-Critical VANETS are composed of multiple nodes each requiring access to a shared communication medium. This access is controlled by the Medium Access Control (MAC) protocol. Numerous MAC protocols have been proposed for VANETS, each with varying degrees of reliability and fairness. A general measure for fairness is required in order to compare different protocols using the same criteria, however, finding a quantifiable measure for fairness is not a simple task and any developed quantifiable measure is application-specific. In this paper, we investigate different measures of fairness, particularly the Jain Index and the Gini Coefficient. We apply these measures to experimental environments in ns-3 to contrast the different fairnesses of three MAC protocols: CSMA/CA, TDMA, and STDMA. It became evident, after experimentation, that the Gini Coefficients obtained from these experiments would vary between iterations and the limits of these variances were uncertain. Therefore we derive a formula which allows a theoretical limit to be placed on the unfairness of a system based on its upper and lower bounds of delay. This formula is not only relevant to VANETs but to any network. The work in this paper is applicable to any discipline wishing to measure the theoretical worst case fairness of a population.

In wireless networks, a message is dropped unexpectedly due to the physical phenomena such as fading, thus requiring a number of backup retransmissions. However, retransmission (which is known to be probabilistic) is mostly disabled in the design of time-triggered communication by the precomputed schedule that reserves every transmission tightly. In this paper, we formally specify the scheduling constraints for a time-triggered wireless network to account for retransmissions in the schedule. We use analytic models of radio propagation to predict the number of retransmissions needed to achieve the desired probability of receiving a packet. Then, the schedule is generated by solving the scheduling constraints by using a Satisfiability Modulo Theory (SMT) solver. We verify the correctness of the resulting schedule to show that our constraints can produce a correct schedule. The performance of the schedule synthesis with different network sizes, topologies, and the number of transmissions are evaluated.

IEC 61499 is a standard for designing industrial control systems using function blocks. Since its publication in 2005, several run-time environments have been developed as plausible implementations. Most of them, however, are poorly suited for use in safety-critical systems, as they are unable to guarantee deterministic behaviour and predictable timing. The use of different run-time environments results in subtle behavioural differences and complicates the effort of static timing analysis. We offer an alternative solution by leveraging the model-based approach to automatically synthesize multirate synchronous programs for a multitasking environment. Our approach preserves the well-known deterministic property of synchronous programs, while facilitating static timing analysis of IEC 61499 specifications. We achieve this without the need to introduce any foreign artefact to the standard. The schedulability criterion for tasks derived using our technique is given for the rate-monotonic scheduling policy. The viability of our approach is demonstrated through a code generator, which synthesizes multirate synchronous code for multi-task execution on the muC/OS-II real-time operating system.

We propose a model-driven approach for designing Wireless Sensor Network (WSN) applications, specifically for systems where hard real-time requirements must be satisfied. Traditionally, developing such systems presents difficulties in ensuring time and timing accuracy due to unpredictable computation time, ambiguities in program concurrency, and behavioural inconsistency between model and implementation. However, in contrast, the models in our approach are fully time-predictable by means of a logical time interval called a tick, while concurrency is automatically handled by the design semantics in a timing guaranteed manner. Meanwhile, the model-driven aspect of automatic code generation guarantees the behavioural consistency between model and implementation. We achieve our approach by using IEC 61499 function blocks and synchronous execution for syntax and semantics respectively. In this paper, we design a time-triggered protocol and a distributed motor synchronization as the network and application layers respectively. Then, we model the overall system for validation by performing composition of such layers. Furthermore, we explain how the logical time tick can be realized during the implementation in a way that the real-time requirement can be satisfied. Finally, the simulation and implementation results demonstrate the effectiveness of our approach.

Synchronous languages are widely used to design safety-critical embedded systems. These languages are based on the synchrony hypothesis, asserting that all tasks must complete instantaneously at each logical time step. This assertion is, however, unsuitable for the design of mixed-criticality systems, where some tasks can tolerate missed deadlines. This paper proposes a novel extension to the synchronous approach for supporting three levels of task criticality: life, mission, and non-critical. We achieve this by relaxing the synchrony hypothesis to allow tasks that can tolerate bounded or unbounded deadline misses. We address the issue of task communication between multi-rate, mixed-criticality tasks, and propose a deterministic lossless communication model. To maximize system utilization, we present a hybrid static and dynamic scheduling approach that executes schedulable tasks during slack time. Extensive benchmarking shows that our approach can schedule up to 15% more task sets and achieve an average of 5.38% better system utilization than the Early-Release EDF (ER-EDF) approach. Tasks are scheduled fairer under our approach and achieve consistently higher execution frequencies, but require more preemptions.

Safety-critical embedded systems, commonly found in automotive, space, and health-care, are highly reactive and concurrent. Their most important characteristics are that they require both functional and timing correctness. C has been the language of choice for programming such systems. However, C lacks many features that can make the design process of such systems seamless while also maintaining predictability. This paper addresses the need for a C-based design framework for achieving time predictability. To this end, we propose the PRET-C language and the ARPRET architecture. PRET-C offers a small set of extensions to a subset of C to facilitate effective concurrent programming. We present a new synchronous semantics for PRET-C. It guarantees that all PRET-C programs are deterministic, reactive, and provides thread-safe communication via shared memory access. This simplifies considerably the design of safety-critical systems. We also present the architecture of a precision timed machine (PRET) called ARPRET. It offers the ability to design time predictable architectures through simple customizations of soft-core processors. We have designed ARPRET particularly for efficient and predictable execution of PRET-C. We demonstrate through extensive benchmarking that PRET-C based system design excels in comparison to existing C-based paradigms. We also qualitatively compare our approach to the Berkeley-Columbia PRET approach. We have demonstrated that the proposed approach provides an ideal framework for designing and validating safety-critical embedded systems.

Synchronous languages ensure determinate concurrency but at the price of restrictions on what programs are considered valid, or constructive . Meanwhile, sequential languages such as C and Java offer an intuitive, familiar programming paradigm but provide no guarantees with regard to determinate concurrency. The sequentially constructive (SC) model of computation (MoC) presented here harnesses the synchronous execution model to achieve determinate concurrency while taking advantage of familiar, convenient programming paradigms from sequential languages. In essence, the SC MoC extends the classical synchronous MoC by allowing variables to be read and written in any order and multiple times, as long as the sequentiality expressed in the program provides sufficient scheduling information to rule out race conditions. This allows to use programming patterns familiar from sequential programming, such as testing and later setting the value of a variable, which are forbidden in the standard synchronous MoC. The SC MoC is a conservative extension in that programs considered constructive in the common synchronous MoC are also SC and retain the same semantics. In this article, we investigate classes of shared variable accesses, define SC-admissible scheduling as a restriction of “free scheduling,” derive the concept of sequential constructiveness, and present a priority-based scheduling algorithm for analyzing and compiling SC programs efficiently.

A system-on-chip (SoC) contains numerous intellectual property blocks, or IPs. Protocol mismatches between IPs may affect the system-level functionality of the SoC. Mismatches are addressed by introducing converters to control inter-IP interactions. Current approaches towards converter generation find limited practical application as they use restrictive models, lack formal rigour, handle a small subset of commonly encountered mismatches, and/or are not scalable. We propose a formal technique for SoC design using incremental converter synthesis . The proposed formulation provides precise models for protocols and requirements, and provides a scalable algorithm that allows adding multiple components and requirements to an SoC incrementally. We prove that the technique is sound and complete. Experimental results obtained using real-life AMBA benchmarks show the scalability and wide range of mismatches handled by our approach.

Synchronous programs have been widely used in the design of safety critical systems such as the flight control of Airbus A-380. To validate the implementations of synchronous programs, it is necessary to map the program's logical time (measured in logical ticks) to physical time (the execution time on a given processor). The static computation of the worst case execution time of logical ticks is called Worst Case Reaction Time (WCRT) analysis. Several approaches for WCRT analysis exist: max-plus algebra, model checking, reachability and integer linear programming (ILP). Of these approaches, reachability, model checking and ILP provide reasonably precise worst case estimates at the expense of longer analysis time. Apart from max-plus based approaches, which can produce large overestimates, the existing approaches suffer from the state space explosion problem. In this paper, we develop a new ILP based approach, called ILPc-which exploits the concurrency explicitly in the ILP formulation to avoid the state space explosion problem. Through extensive bench-marking we demonstrate the efficacy of the approach: for complex programs, ILPc is often orders of magnitude faster compared to the existing approaches, while achieving same level of precision. Thus, this paper paves the way for scalable WCRT analysis of complex embedded systems designed using the synchronous approach.

Safety-critical systems require guarantees on their worst-case execution times. This requires modelling of speculative hardware features such as caches that are tailored to improve the average-case performance, while ignoring the worst case, which complicates the Worst Case Execution Time (WCET) analysis problem. Existing approaches that precisely compute WCET suffer from state-space explosion. In this paper, we present a novel cache analysis technique for direct-mapped instruction caches with the same precision as the most precise techniques, while improving analysis time by up to 240 times. This improvement is achieved by analysing individual control points separately, and carrying out optimisations that are not possible with existing techniques.

The web service community has introduced many techniques to cope with the inability of WSDL to describe a service's behavior. Those techniques range from embedding more XML tags in WSDL, to generate formal behavioral models on top of WSDL. Apart from the efficiency of these techniques, a common problem is that they require manual efforts to model the behavior of a service, and often need informal documentation from service vendors to do so. In this paper, we propose a solution for the above problem by automatically extracting a service's behavior, directly from its WSDL document. Our approach is based on the utilization of particular WSDL elements, which are usually ignored by bottom-up approaches while generating a WSDL file. We illustrate our process in steps by taking a scenario from Amazon E-commerce Web Service. We also survey the issues with extracting the behavioral models, from the WSDLs of existing web services. Finally, we tested our automatically generated models by composing them together using our service composition framework.

Systems-on-chip (SoCs) contain multiple interconnected and interacting components. In this paper, we present a compositional approach for the integration of multiple components with a wide range of protocol mismatches into a single SoC. We show how SoC construction can be done in single-step when all components are integrated at once or it can also be performed incrementally by adding components to an already integrated design. Using a number of AMBA IPs, we show that the proposed framework is able to perform protocol conversion in many cases where existing approaches fail.

The strict requirements of embedded control software, in the absence of a formal approach, necessitates ad-hoc optimisations and coding decisions in the “C” language. Model driven development (MDD) is a proposed methodology for alleviating problems inherent in this method. We propose an IEC 61499 model based approach for the reengineering of existing or legacy industrial embedded systems. Experimental evidence and hands-on experience is used to illustrate the challenges faced by adopting such an approach; primarily, the lacuna that exists between current standards and industry practices. Several syntactic enhancements based on a layered approach are proposed to address these concerns.

Cyber-physical systems (CPS) are integrations of computation and control with sensing and actuation of the physical environment. Typically, such systems consist of embedded computers that monitor and control physical processes in a feedback loop. While modern electronic systems are increasingly characterized as CPS, their design and synthesis still rely on traditional methods, which lack systematic and automated techniques for accomplishment. Recently, IEC 61499 has been proposed as a standard for designing industrial process-control and measurement systems. It prescribes a component-based approach for developing industrial automation software using function blocks. Executable code can then be automatically generated and simulated from these function blocks. This bodes well for designers of CPS, who are more likely to be experts in specific industrial domains, rather than in computer science. The intuitive graphical nature and automatic code synthesis of IEC 61499 programs will alleviate the programming burden of industrial engineers, while ensuring more reliable software. While software synthesis from IEC 61499 programs is not new, the generation of efficient code from them has been wanting. This has made it difficult for function blocks to be used in software development for resource-constrained embedded controllers commonly employed in CPS. To address this, we present an approach that can generate very efficient code from function block descriptions. Experimental results from a benchmark suite shows that our approach produces substantially faster and smaller code compared to existing techniques.

The IEC 61499 standard defines a generic architecture for designing distributed industrial control systems based on function blocks. The standard, however, lacks a formal model of computation to describe the behavior of function block compositions. While various models have been prescribed in the literature to define the composite behavior on a single computational node, few have been proposed to directly address compositions in a distributed setting. This paper proposes a globally asynchronous locally synchronous (GALS) model for distributed function block systems. The model provides an abstract way to view communication between function blocks without implying yet any particular implementation. This abstraction can then be subsequently refined to obtain various implementations with different tradeoffs. We do so using an approach that is fully compatible with the standard's notion of communication function blocks, which abstract underlying communication mechanisms from the application. As a contribution, we have developed a compiler that automatically synthesizes separate programs for a given distributed function block system without needing any additional middleware or run-time environment to execute the resulting distributed code. The efficacy of the proposed approach is demonstrated through an industrial case study.

Static computation of the worst-case reaction time (WCRT) is required for the real-time execution of synchronous programs. Existing approaches use model checking or integer linear programming. we formulate this as an abstraction-based reachability analysis yielding a lower worst case complexity. Benchmarking shows a significant overall speed-up of 64-times over existing approaches.

Synchronous programs execute in discrete instants, called ticks. For real-time implementations, it is important to statically determine the worst case tick length, also known as the worst case reaction time (WCRT). While there is a considerable body of work on the timing analysis of procedural programs, such analysis for synchronous programs has received less attention. Current state-of-the art analyses for synchronous programs use integer linear programming (ILP) combined with path pruning techniques to achieve tight results. These approaches first convert a concurrent synchronous program into a sequential program. ILP constraints are then derived from this sequential program to compute the longest tick length. In this paper, we use an alternative approach based on model checking. Unlike conventional programs, synchronous programs are concurrent and state-space oriented, making them ideal for model checking based analysis. We propose an analysis of the abstracted state-space of the program, which is combined with expressive data-flow information, to facilitate effective path pruning. We demonstrate through extensive experimentation that the proposed approach is both scalable and about 67% tighter compared to the existing approaches.

Esterel is a synchronous language suited for describing reactive embedded systems. It combines fine-grained parallelism with precise timing control for the execution of threads. Due to this, Esterel programs have typically been compiled into sequential code in software implementations, as tight synchronization between a large number of threads cannot be efficiently managed with an operating system (OS). This has enabled concurrent Esterel programs to be executed directly on single-core processors. Recently, however, multi-core processors have been increasingly used to achieve better performance in embedded applications. The conventional approach of generating sequential code from Esterel programs is unable to take advantage of multi-core processors. We overcome this limitation by compiling Esterel into a limited number of thread partitions (up to the number of available cores) to avoid the large overheads of implementing each Esterel thread separately within a conventional multithreading scheme. These partitions are then distributed onto separate cores using a static load balancing heuristic. The Esterel threads within a partition may then be dynamically scheduled with or without an OS. To evaluate the viability of this approach, we present experimental results comparing the execution of a set of benchmarks using one to four cores on the Intel Core 2 Quad with Linux, and one to two cores on the Xilinx Micro blaze without any OS. We have performed extensive benchmarking over large Esterel programs to illustrate that achieving throughput with parallel execution of Esterel is benchmark dependent.

The use of formal models of computation in dealing with increasing complexity of embedded systems design is gaining attention. A successful model of computation must be able to handle both control-dominated and data-dominated behaviors, which are most often simultaneously present in complex embedded systems. Besides behavioral heterogeneity, direct support for modeling distributed systems is also desirable, since an increasing number of embedded systems belong to this category. In this paper, we present distributed DFCharts (DDFCharts), a language based on a formal model that targets distributed heterogeneous embedded systems. Its top hierarchical level is made suitable to capture distributed systems. Behavioral heterogeneity is addressed by composing finite-state machines (FSMs) and synchronous dataflow graphs (SDFGs). We illustrate modeling in DDFCharts with practical examples and describe its implementation on heterogeneous target architecture.

We present a new language called Precision Timed C, for predictable and lightweight multithreading in C. PRET-C supports synchronous concurrency, preemption, and a high-level construct for logical time. In contrast to existing synchronous languages, PRET-C offers C-based shared memory communications between concurrent threads, which is guaranteed to be thread safe via the proposed semantics. Mapping of logical time to physical time is achieved by a Worst Case Reaction Time (WCRT) analyser. To improve throughput while maintaining predictability, a hardware accelerator specifically designed for PRET-C is added to a soft-core processor. We then demonstrate through extensive benchmarking that the proposed approach not only achieves complete predictable execution, but also improves overall throughput when compared to the software execution of PRET-C. The PRET-C software approach is also significantly more efficient in comparison to two other light-weight concurrent C variants called SC and Protothreads, as well as the well-known synchronous language Esterel.

We propose a new language called Precision Timed C (PRET-C), for predictable and lightweight multi-threading in C. PRET-C supports synchronous concurrency, preemption, and a high-level construct for logical time. In contrast to existing synchronous languages, PRET-C offers C-based shared memory communications between concurrent threads that is guaranteed to be thread safe. Due to the proposed synchronous semantics, the mapping of logical time to physical time can be achieved much more easily than with plain C, thanks to a Worst Case Reaction Time (WCRT) analyzer (not presented here). Associated to the PRET-C programming language, we present a dedicated target architecture, called ARPRET, which combines a hardware accelerator associated to an existing softcore processor. This allows us to improve the throughput while preserving the predictability. With extensive benchmarking, we then demonstrate that ARPRET not only achieves completely predictable execution of PRET-C programs, but also improves the throughput when compared to the pure software execution of PRET-C. The PRET-C software approach is also significantly more efficient in comparison to two other light-weight concurrent C variants (namely SC and Protothreads), as well as the well-known Esterel synchronous programming language.

Accurate estimation of the tick length of a synchronous program is essential for efficient and predictable implementations that are devoid of timing faults. The techniques to determine the tick length statically are classified as worst case reaction time (WCRT) analysis. While a plethora of techniques exist for worst case execution time (WCET) analysis of procedural programs, there are only a handful of techniques for determining the WCRT value of synchronous programs. Most of these techniques produce overestimates and hence are unsuitable for the design of systems that are predictable while being also efficient. In this paper, we present an approach for the accurate estimation of the exact WCRT value of a synchronous program, called its tight WCRT value, using model checking. For our input specifications we have selected a synchronous C based language called PRET-C that is designed for programming Precision Timed (PRET) architectures. We then present an approach for static WCRT analysis of these programs via an intermediate format called TCCFG. This intermediate representation is then compiled to produce the input for the model checker.

The automated design of SoCs from pre-selected IPs that may require different clocks is challenging because of the following issues. Firstly, protocol mismatches between IPs need to be resolved automatically before IPs are integrated. Secondly, the presence of multiple clocks makes the protocol conversion even more difficult. Thirdly, it is desirable that the resulting integration is correct-by-construction, i.e., the resulting SoC satisfies given system-level specifications. All of these issues have been studied extensively, although not in a unifying manner. In this paper we propose a framework based on protocol conversion that addresses all these issues. We have extensively studied many SoC design problems and show that the proposed methodology is capable of handling them better than other known approaches. A significant contribution of the proposed approach is that it nicely generalizes many existing techniques for formal SoC design and integrates them into a single approach.

The IEC 61499 function block standard proposes a new specification language for describing distributed industrial control systems. The standard specifies the use of an execution control chart (ECC) for state control, with algorithm calls for data handling. The design of complex industrial systems such as baggage handling systems can be difficult because of large state-spaces or complicated component interactions. Additionally, the flat state machines used in the standard do not provide a simple method for specifying error handling within the process's execution. State machines from synchronous languages, however, have hierarchy and concurrent constructs to aid the developer. This paper presents a hierarchical and concurrent extension to ECCs, which we call HCECCs, which presents new design constructs adapted from synchronous languages in order to improve system specification with function blocks. The semantics of HCECCs, which are backward compatible with the standard, are described and design using HCECCs is compared with other specification approaches.

IEC 61499 has been endorsed as the standard for modeling and implementing distributed industrial process measurement and control systems. The standard prescribes the use of function blocks for designing systems in a component-oriented approach. The execution model of a basic function block and the manner for event/data connections between blocks are described therein. Unfortunately, the standard does not provide exhaustive specifications for function block execution. Consequently, multiple standard-compliant implementations exhibiting different behaviors are possible. This not only defeats the purpose of having a standard but also makes verification of function block systems difficult. To overcome this, we propose synchronous semantics for function blocks and show its feasibility by translating function blocks into a subset of Esterel, a well-known synchronous language. The proposed semantics avoids causal cycles common in Esterel and is proved to be reactive and deterministic under any composition. Moreover, verification techniques developed for synchronous systems can now be applied to function blocks.

SystemJ is a language based on the Globally Asynchronous Locally Synchronous (GALS) paradigm. A SystemJ program is a collection of GALS nodes, also called clock domains, and each clock domain is a synchronous program that extends the Java language. Initial compilation of SystemJ has been to standard Java executing on a Java Virtual Machine (JVM), which is both inefficient and bulky for small embedded systems. This article proposes a new approach for compiling and executing SystemJ using a new type of virtual machine, called a Tandem Virtual Machine (TVM). The TVM approach provides an efficient implementation of SystemJ on both standard processors and resource-constrained embedded processors. The new approach is based on separating the control-driven and data-driven operations for execution on two virtual machines. While the JVM executes the data-driven operations, a Control Virtual Machine (CVM) is introduced to execute the control-driven parts of a SystemJ program. The TVM approach is capable of handling all data-driven and control-driven operations required by the GALS model. The benchmark results show that the TVM has code size improvements of over 60% on average and also a substantial improvement in execution speed over standard Java-based compilation.

Single-clock specifications with purely synchronous communication have been successfully used in capturing the behavior of small and medium scale embedded systems. In large scale embedded systems, where processes often operate at vastly different speeds, using a single clock in an entire specification can be difficult. In this paper, we present Multiclock Charts (McCharts), a language where finite state machines driven by different clocks are composed. The communication between FSMs is specified by both synchronous and asynchronous mechanisms. The essential feature in the semantics of McCharts is that a complete specification can be mapped onto a single multiclock FSM (MCFSM).

In this paper, we propose a new system-level design language, called SystemJ. It extends Java with synchronous reactive features present in Esterel and asynchronous constructs suitable for modelling globally asynchronous locally synchronous systems. The strength of SystemJ comes from its ability to offer the data processing and encapsulation elegance of Java, Esterel-like reactivity and synchrony, and the asynchronous de-coupling of CSP all within the Java framework. Using standard Java environments, for specification and modelling, or specialised reactive embedded processors, for high performance implementation, the SystemJ design flow is extremely versatile. With the increasing attention that Java gets in embedded systems, SystemJ comes to address data and control, software and hardware, modelling and implementation in a unified manner

Efficient scheduling mechanisms are essential for implementing real-time operating systems on embedded microprocessors. Reactive processors provide mechanisms and an instruction set architecture more suitable for dealing with external signals than it is the case with traditional interrupts. By extending the reactive framework further we demonstrate simple and efficient hardwareimplemented scheduling of tasks with static priorities. The scheduler support unit is added to the reactive microprocessor core. The real-time scheduler shows substantial improvement of performance over the conventional approach of using prioritized interrupts.

Reactivity on external events is an important feature of almost all embedded systems. In this paper we present the design of a new, reactive embedded microprocessor called REMIC, that supports reactivity in a new way following the paradigm of synchronous system level language Esterel. The rationale for REMIC design, its novel features with the design details and some performance figures are presented to demonstrate its suitability for embedded systems. Besides single processor systems, REMIC can be easily combined into multiple processor architectures that support real concurrency.

Specification of embedded systems based on formal models of computation is gaining importance. The behavior of an increasing number of embedded systems is heterogeneous, consisting of a mixture of control-dominated and data-dominated parts. While models of computations suitable to control-dominated systems and data-dominated systems are well developed, there are only a limited number of models catering to both systems. In this paper, we present informally a new model for heterogeneous embedded systems, called HEMOC, which combines three common models of computation, synchronous reactive, hierarchical finite state machines and synchronous data flow. Then, the languages Esterel and SyncCharts are used for system specification following the new model in order to determine what they need to become suitable specification platform.

Esterel is a system-level language for the modelling, verification and synthesis of control dominated (reactive) embedded systems. Existing Esterel compilers generate intermediate C code that is subsequently mapped to a suitable target processor. The generated code emulates the reactive features of the language due to lack of support for these features on traditional processors. The resultant code is thus inefficient and bulky. Therefore, Esterel is not so effective for resource constrained embedded systems. This paper describes a reactive microcontroller called RePIC that has native support for reactive features of the language. Limited support for concurrent Esterel programs is demonstrated through a dual-processor RePIC architecture. A new benchmark suite for comparing the reactive performance of processors called the Auckland Reactive Benchmark (ARE-Bench) is used to demonstrate significant performance improvement and code compaction due to the proposed approach. This paper, thus, paves the way for resource constrained embedded system development using a subset of Esterel supported by RePIC like architectures.

Automatic IP (Intellectual Property) matching is a key to reuse of IP cores. This paper presents an IP matching algorithm that can check whether a given programmable IP block can be adapted to match a given specification. When such adaptation is possible, the algorithm also generates a device driver to adapt the IP block. Though simulation, refinement and bisimulation based algorithms exist, they cannot be used to check the adaptability of an IP block, which is the essence of reuse. The IP matching algorithm is based on a formal verification technique called k-time forced simulation proposed in this paper k-time forced simulation may be used for identifying whether a given IP block (a device D) can be adapted to match a specification (a function F), given that D has a clock that is k-times faster than F. We demonstrate the applicability of the algorithm by reusing several IP blocks.

Synchronous languages may be used for specification and design of embedded systems. Assuming the availability of a library of synchronous programs, we propose a technique to enable reuse of these programs, via an algorithm for automatic matching of a design function to a program from the library. The algorithm, when successful, generates an interface which automatically adapts the program. The algorithm is based on a new simulation relation called synchronous forced simulation, which is shown to be necessary and sufficient for matching a given pair of function and program.

Component reuse techniques have been a recent focus of research because they are seen as the next-generation techniques to handle increasing system complexities. However, there are several unresolved issues to be addressed and prominent among them is the issue of component matching . As the number of reusable components in a component database grows, the task of manually matching a component to the user requirements becomes infeasible. Automating this matching can help in rapid system prototyping, improving quality and reducing cost. In addition, if the matching algorithm is sound, this approach can also reduce precious validation effort.In this article, we propose an algorithm for automatic matching of a design function to a device from a component database. The distinguishing feature of the algorithm is that when successful, it generates an interface that can automatically adapt the device to behave as the function. The algorithm is based on a new simulation relation called forced simulation that is shown to be a necessary and sufficient condition for component matching to be possible for a given pair of function and device. We demonstrate the application of the algorithm by reusing on some programmable components of the Intel family.

Embedded systems are application specific digital systems that are usually designed using a microprocessor, along with a set of programmable hardware and software components. Since these systems are real time in nature, specification of temporal constraints is a key issue. We have recently proposed the CFSMcharts language for component based specification of these systems. However this proposal had no features to specify quantitative temporal constraints that are crucial to embedded system specification. We propose a new model of time, called hidden time, for specification of temporal constraints in CFSMcharts and contrast it with existing schemes. The proposed scheme is hierarchical and hides away the quantitative temporal constraints from the top level specification. This leads to a simpler style for the specification of these constraints and simpler semantics for the top level specification. Another major contribution of the proposed scheme is that properties to be verified can be expressed in propositional temporal logic, whereas all the existing schemes have to use first order temporal logic. We also propose a new temporal logic called Hidden Propositional Temporal Logic (HPTL) as a requirement specification language. HPTL is based on the hidden time model and also supports module name qualifiers, which have applicability in a component based framework. Finally, we propose a scheme for automated verification.

In CAD systems, it is often required to implement desired behaviors by some available device. The selection of the device that can implement the behavior, and the required interfacing, is usually done by human experts. The interface consists of transformations that may have to be performed on the inputs and outputs of the device. This paper describes an approach to automatically derive the specifications of the device's interface. For sequential circuits, the behaviors are often represented as FSMs, and hence the task is to determine whether the FSM of the desired function can be contained in the FSM of the device, subject to the transformations of the interface. A related objective, addressed in this paper, is to model the behaviors of complex devices in a way that facilitates the analysis.