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.

Synchronous programs are used to implement safety critical embedded software. Efficiently compiling imperative synchronous programs into small and fast executables is challenging, due to state-space explosion. This paper introduces a novel linear time compilation technique for automata based compilation of synchronous programs. Graph based rewrite rules for kernel programming constructs are introduced. The compiled program is encoded into a type-state program using template meta-programming in C++. Experimental results show that the compilation time and generated binary size is comparable, while the execution times are on average 31–60% faster than current state-of-the-art compilers.

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.

Abstract Bitcoin (BTC) perpetual futures contracts are highly leveraged speculative trading instruments with daily market trading of $45 Billion. BTC perpetual futures are derivative contracts, which depend upon the underlying BTC SPOT (current) price. Pricing perpetual futures fairly is hard, using traditional arbitrage arguments, because of the volatile nature of the so called funding rate, which is used as the replacement of risk free rate in the Cryptocurrency market. This work presents a novel technique for pricing BTC futures contracts using conditional volatility and mean models. Intra‐day high‐frequency futures' return volatility and mean are modelled using different ML and econometric techniques. A comparison is made using statistical measures to find the model that best captures the intra‐day conditional mean and volatility. Exponential generalized autoregressive conditional heteroskedasticity is shown to be an almost unbiased predictor of intra‐day volatility, while a constant autoregressive moving average (0, 0) model best captures the conditional mean of the returns. A market directional high frequency trading algorithm is developed using the volatility and mean models. The algorithm first prices the futures contract at some future point of time using the volatility and mean regression models. Next, the slope between the current futures price and the expected price are used to predict the market direction. A long or short position is taken depending upon the expected market direction movement. Extensive back‐testing results show absolute returns of 1500%–8000% depending upon the transaction fees and leverage used. On average, the market direction is predicted correctly 85% of the time by the best model. Finally, the trading technique is market neutral, in that it gives large positive returns, with low SD, in both bull and bear markets.

Designing software systems underpinned by a formal model of computation (MoC) is crucial for safety-critical, real-time and all industrial applications as it allows formal analysis of those designs and support for correct by design systems. In this paper, we focus on Globally Asynchronous Locally Synchronous (GALS) software systems and Coloured Petri Nets (CPNs) based approach to formally model and analyse GALS software systems specified in SystemJ GALS programming language. The approach translates SystemJ constructs into CPN modules and composes them into CPN GALS model based on control flow and concurrency specified in the SystemJ program. It preserves GALS MoC by automatically integrating synchronizer modules, asynchronous channel interface modules, and scheduling modules to result in the execution model of SystemJ program equivalent CPN. The created CPN GALS model allows system developers to verify the properties of the design formally with the use of Computation Tree Logic (CTL). An industrial automation example is provided as a use case.

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.

OBJECTIVE: To develop, train and test neural networks for predicting heart surface potentials (HSPs) from body surface potentials (BSPs). The method re-frames traditional inverse problems of electrocardiography into regression problems, constraining the solution space by decomposing signals with multidimensional Gaussian impulse basis functions. METHODS: Impulse HSPs were generated with single Gaussian basis functions at discrete heart surface locations and projected to corresponding BSPs using a volume conductor torso model. Both BSP (inputs) and HSP (outputs) were mapped to regular 2D surface meshes and used to train a neural network. Predictive capabilities of the network were tested with unseen synthetic and experimental data. RESULTS: A dense full connected single hidden layer neural network was trained to map body surface impulses to heart surface Gaussian basis functions for reconstructing HSP. Synthetic pulses moving across the heart surface were predicted from the neural network with root mean squared error of 9.1±1.4%. Predicted signals were robust to noise up to 20 dB and errors due to displacement and rotation of the heart within the torso were bounded and predictable. A shift of the heart 40 mm toward the spine resulted in a 4% increase in signal feature localization error. The set of training impulse function data could be reduced, and prediction error remained bounded. Recorded HSPs from in-vitro pig hearts were reliably decomposed using space-time Gaussian basis functions. Activation times calculated from predicted HSPs for left-ventricular pacing had a mean absolute error of 10.4±11.4 ms. Other pacing scenarios were analyzed with similar success. CONCLUSION: Impulses from Gaussian basis functions are potentially an effective and robust way to train simple neural network data models for reconstructing HSPs from decomposed BSPs. SIGNIFICANCE: The HSPs predicted by the neural network can be used to generate activation maps that non-invasively identify features of cardiac electrical dysfunction and can guide subsequent treatment options.

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.

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.

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.

SystemJ is a programming language developed for implementing safety critical cyber-physical systems, including industrial automation systems. However, the current tools do not support an efficient mechanism to verify SystemJ programs formally. This paper presents a semantics-preserving translation of the synchronous subset of SystemJ to Coloured Petri Net (CPN), which in turn enables leveraging the plethora of analysis and verification tools for CPN to verify SystemJ programs. The translation and verification approach is illustrated on a pedagogical industrial automation example of a SystemJ program.

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.

Online Peer to Peer Lending (P2PL) systems connect lenders and borrowers directly, thereby making it convenient to borrow and lend money without intermediaries such as banks. Many recommendation systems have been developed for lenders to achieve higher interest rates and avoid defaulting loans. However, there has not been much research in developing recommendation systems to help borrowers make wise decisions. On P2PL platforms, borrowers can either apply for bidding loans, where the interest rate is determined by lenders bidding on a loan or traditional loans where the P2PL platform determines the interest rate. Different borrower grades — determining the credit worthiness of borrowers get different interest rates via these two mechanisms. Hence, it is essential to determine which type of loans borrowers should apply for. In this paper, we build a recommendation system that recommends to any new borrower the type of loan they should apply for. Using our recommendation system, any borrower can achieve lowered interest rates with a higher likelihood of getting funded.

Online P2PL systems allow lending and borrowing between peers without the need for intermediaries such as banks. Convenience and high rate of returns have made P2PL systems very popular. Recommendation systems have been developed to help lenders make wise investment decisions, lowering the chances of overall default. However, P2PL marketplace suffers from low financial liquidity, i.e., loans of different grades are not always available for investment. Moreover, P2PL investments are long term (usually a few years), hence, incorrect investment cannot be liquidated easily. Overall, the state-of-the-art recommendation systems do not account for the low market liquidity and hence, can lead to unwise investment decisions. In this paper we remedy this shortcoming by building a recommendation framework that builds an investment portfolio, which results in the highest return and the lowest risk along with a statistical measure of the number of days required for the amount to be completely funded. Our recommendation system predicts the grade and number of loans that will appear in the future when constructing the investment portfolio. Experimental results show that our recommendation engine outperforms the current state-of-the-art techniques. Our recommendation system can increase the probability of achieving the highest return with the lowest risk by ~ 69%.

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.

An especially daunting challenge of scheduling real-time applications on multiprocessor system on chip (MPSoC) is to incorporate timing anomalies due to access contention to shared resources. Time division multiplex arbitration (TDMA) provides static timing guarantees at the cost of significant loss in the average case performance of the application. This paper presents a shared resource contention arbitration approach allowing high bus utilization while guaranteeing WCET values for all tasks in the real-time application. The paper includes performance results obtained by executing hard real-time applications on a MPSoC with shared memory connected to the processors via a shared bus, implemented on a FPGA. The results show that the proposed approach provides: 1 bus bandwidth utilization close to static priority based arbitration, 2 a fairer bandwidth distribution compared to round robin arbitration, and 3 latency guarantees identical to TDMA.

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.

Time predictability is a first class requirement in safety critical system design. Techniques exist for the timing analysis of programs designed in memory managed languages, but these require detailed knowledge of memory allocation. Moreover, enforcing hard real-time guarantees for systems designed in such garbage collected languages is difficult, because of the so called collection pause - however incremental. This paper proposes a novel solution whereby a separate reference counting unit replaces the garbage collector. We present the underlying concepts of the Reference Counting Memory Management Unit (RCMMU) and its use for garbage collection. In addition, we present an implementation that includes a specialized memory arrangement that allows for object management transactions to occur concurrently with program execution, with no resultant impact upon program performance. The RCMMU has been targeted for use with Java but can be adopted to be used with other memory managed languages. The hardware-implemented RCMMU removes all overhead associated with garbage collection operations when compared against a software-only collector. Additionally, it simplifies the static worst-case execution time analysis of programs.

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.

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.

Scalability and performance in multicore processors for embedded and real-time systems usually don't go well each with the other. Networks on Chip (NoCs) provide scalable execution platforms suitable for such kind of embedded systems. This article presents a NoC-based Heterogeneous Multi-Processor system, called NoC-HMP, which is a scalable platform for embedded systems developed in the GALS language SystemJ. NoC-HMP uses a time-predictable TDMA-MIN NoC to guarantee latencies and communication time between the two types of time-predictable cores and can be customized for a specific performance goal through the execution strategy and scheduling of SystemJ program deployed across multiple cores. Examples of different execution strategies are introduced, explored and analyzed via measurements. The number of used cores can be minimized to achieve the target performance of the application. TDMA-MIN allows easy extensions of NoC-HMP with other cores or IP blocks. Experiments show a significant improvement of performance over a single core system and demonstrate how the addition of cores affects the performance of the designed system.

Automatically exploiting short vector instructions sets (SSE, AVX, NEON) is a critically important task for optimizing compilers. Vector instructions typically work best on data that is contiguous in memory, and operating on non-contiguous data requires additional work to gather and scatter the data. There are several varieties of non-contiguous access, including interleaved data access. An existing approach used by GCC generates extremely efficient code for loops with power-of-2 interleaving factors (strides). In this paper we propose a generalization of this approach that produces similar code for any compile-time constant interleaving factor. In addition, we propose several novel program transformations, which were made possible by our generalized representation of the problem. Experiments show that our approach achieves significant speedups for both power-of-2 and non--power-of-2 interleaving factors. Our vectorization approach results in mean speedups over scalar code of 1.77x on Intel SSE and 2.53x on Intel AVX2 in real-world benchmarking on a selection of BLAS Level 1 routines. On the same benchmark programs, GCC 5.0 achieves mean improvements of 1.43x on Intel SSE and 1.30x on Intel AVX2. In synthetic benchmarking on Intel SSE, our maximum improvement on data movement is over 4x for gathering operations and over 6x for scattering operations versus scalar code.

The Semantic Web comprises enormous volumes of semi-structured data elements. For interoperability, these elements are represented by long strings. Such representations are not efficient for the purposes of applications that perform computations over large volumes of such information. A common approach to alleviate this problem is through the use of compression methods that produce more compact representations of the data. The use of dictionary encoding is particularly prevalent in Semantic Web database systems for this purpose. However, centralized implementations present performance bottlenecks, giving rise to the need for scalable, efficient distributed encoding schemes. In this paper, we propose an efficient algorithm for fast encoding large Semantic Web data. Specially, we present the detailed implementation of our approach based on the state-of-art asynchronous partitioned global address space (APGAS) parallel programming model. We evaluate performance on a cluster of up to 384 cores and datasets of up to 11 billion triples (1.9 TB). Compared to the state-of-art approach, we demonstrate a speed-up of$2.6 - 7.4\times$and excellent scalability. In the meantime, these results also illustrate the significant potential of the APGAS model for efficient implementation of dictionary encoding and contributes to the engineering of more efficient, larger scale Semantic Web applications.

This paper presents an extensible and adaptable platform for distributed applications with mixed criticality based on using state of the art FPGA technology. Although capable of executing programs written in different languages, the platform specifically targets the execution of programs written in Globally Asynchronous Locally Synchronous language SystemJ used in the context of Internet of Industrial Things. The key properties of the prototype platform are accommodation of mixed-criticality processing as well as provision of Internet addressable services. Mixed-criticality execution platform (MCEP) uses multiple processor cores and network interfaces: (1) a dual-core ARM processor with Ethernet for Internet access and processing of non-real -- time application parts and (2) TP-JOP reactive hard real-time processor with customized Controller Area Network (CAN) for real-time and time-critical response processing. This platform has been successfully developed and used in an industrial automation system within the Internet of Industrial Things context.

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.

In this article, we partition and scheduleSynchronous Dataflow(SDF) graphs onto heterogeneous execution architectures in such a way as to minimize energy consumption and maximize throughput. Partitioning and scheduling SDF graphs onto homogeneous architectures is a well-known NP-hard problem. The heterogeneity of the execution architecture makes our problem exponentially challenging to solve. We model the problem as a weighted sum and solve it using novel state space exploration inspired from the theory of parallel automata. The resultant heuristic algorithm results in good scheduling when implemented in an existing stream framework.

Safety-critical software systems need to guarantee functional correctness and bounded response times to external input events. Programs designed using reactive programming languages, based on formal mathematical semantics, can be automatically verified for functional correctness guarantees. Real-time guarantees on the other hand are much harder to achieve. In this article we provide a static analysis framework for guaranteeing response times for reactive programs developed using the Globally Asynchronous Locally Synchronous (GALS) model of computation. The proposed approach is applicable to scheduling of GALS programs for different target architectures with single or multiple processors or cores. A Satisfiability Modulo Theory (SMT) formulation in the quantifier free linear real arithmetic (QF_LRA) logic is used for scheduling. A novel technique to encode rendezvous used in synchronization of globally asynchronous processes in the presence of locally synchronous parallelism and arbitrary preemption into QF_LRA logic is presented. Finally, our SMT formulation is shown to produce schedules in reasonable time.

We present a novel approach for design of manufacturing automation systems with formal verification of selected properties based on the use of Globally Asynchronous Locally Synchronous programming language SystemJ and industrial-proof verification tools. By being able to prove properties of the automation control logic that consists of multiple concurrent controllers, represented by FSMs that correspond to asynchronous processes of SystemJ program, using Spin model checker, we demonstrate that the program features can be formally verified. Moreover, by also guaranteeing preservation of features and GALS model of the SystemJ program after compilation (correct by construction specification), we actually close the design process within What You Prove Is What You Execute (WYPIWYE) Paradigm.

We present a simulated annealing based partitioning technique for mapping task graphs, onto heterogeneous processing architectures. Task partitioning onto homogeneous architectures to minimize the makespan of a task graph, is a known NP-hard problem. Heterogeneity greatly complicates the aforementioned partitioning problem, thus making heuristic solutions essential. A number of heuristic approaches have been proposed, some using simulated annealing. We propose a simulated annealing method with a novel NEXT STATE function to enable exploration of different regions of the global search space when the annealing temperature is high and making the search more local as the temperature drops. The novelty of our approach is two fold: (1) we go a step further than the existing scientific literature, considering heterogeneity at levels of task parallelism, data parallelism and communication. (2) We present a novel algorithm that uses simulated annealing to find better partitions in the presence of heterogeneous architectures, data parallel execution units, and significant data communication costs. We conduct a statistical analysis of the performance of the proposed method, which shows that our approach clearly outperforms the existing simulated annealing method.

Static estimation of the Worst Case Reaction Time (WCRT) of synchronous programs is pivotal for designing hard-real time systems in these languages. The current approaches to WCRT estimation suffer from either large overestimation of the WCRT value or the state space explosion problem. In this paper, we present TACO: a framework that integrates model checking based WCRT estimation with code optimization techniques, which results in close to optimal WCRT estimates with orders of magnitude reduced worst case runtime complexity. Finally, the TACO framework also allows us to generate executables with a smaller overall memory footprint.

In this paper we introduce exact and non-exact real-time waits in reactive Globally Asynchronous Locally Synchronous (GALS) programming languages and synchronous languages as their subset. The language constructs that allow use of real-time waits are illustrated on the SystemJ GALS language. They allow system designers to explicitly use, at the specification level, not only logical time but also the real-time in order to control program execution. The introduced concepts utilize execution platforms that allow finding best and worst reaction time of a GALS or synchronous program.

In this article we use model checking to statically distribute and schedule Synchronous DataFlow (SDF) graphs on heterogeneous execution architectures . We show that model checking is capable of providing an optimal solution and it arrives at these solutions faster (in terms of algorithm runtime) than equivalent ILP formulations. Furthermore, we also show how different types of optimizations such as task parallelism, data parallelism, and state sharing can be included within our framework. Finally, comparison of our approach with the current state-of-the-art heuristic techniques show the pitfalls of these techniques and gives a glimpse of how these heuristic techniques can be improved.

We present a new heterogeneous multiprocessor (GALS-HMP) for the execution of Globally Asynchronous Locally Synchronous (GALS) programming languages. It specifically targets SystemJ GALS language, which extends Java with asynchronous and synchronous concurrency. A SystemJ program is partitioned by a compiler onto data-driven and control-driven parts, which are then allocated for the execution on traditional and reactive processors, which constitute GALS-HMP. The reactive processor is customized to meet the requirements of the control parts of the SystemJ programs. The prototypes developed on an FPGA show significant improvements in code size and execution speed compared to the case of using just traditional processors.

Distributed surveillance systems represent a class of sensor networks used for object location and tracking, road traffic monitoring, security, and other purposes. They are very complex to describe, design, and run. Because of their sensitivity, they need to be carefully designed and validated. We present a system-level approach to modeling and designing such systems using a new system-level programming language, SystemJ, which enables designers to describe computational and communication parts of such applications in a highly abstract manner. The designed system can be modeled and validated even before deployment and in that way contribute to the overall reliability and trustworthiness of such systems. As an additional tool, the design environment for specification of the surveillance system topology, physical and communication properties, selected sensors and their interconnectivity with the computing resources was developed. This tool enables easy composition of multiple sensors and their respective controllers, capturing changes of configuration of the system and underlying communication, and automatic generation of the formal description of the surveillance system. This description is then used for the generation of executable code and/or the templates for detailed SystemJ application-specific code, as well as for generation of the operator GUI in a surveillance system.

The paper presents a programming language, DSystemJ, for dynamic distributed Globally Asynchronous Locally Synchronous (GALS) systems, its formal model of computation, formal syntax and semantics, its compilation and implementation. The language is aimed at dynamic distributed systems, which use socket based communication protocols for communicating between components. DSystemJ allows the creation and control at runtime of asynchronous processes called clock-domains, their mobility on a distributed execution platform, as well as the runtime reconfiguration of the system's functionality and topology. As DSystemJ is based on a GALS model of computation and has a formal semantics, it offers very safe mechanisms for implementation of distributed systems, as well as potential for their formal verification. The details and principles of its compilation, as well as its required runtime support are described. The runtime support is implemented in the SystemJ GALS language that can be considered as a static subset of DSystemJ.

LibGALS is a library and run-time environment that extends a multi-process host operating system (OS) to support the design of Globally Asynchronous Locally Synchronous (GALS) software systems and models. LibGALS provides an application programming interface (API) that enables the designer to describe GALS concurrent programs and reactivity in sequential programming languages. Moreover, it facilitates the interface between the GALS concurrent program and other processes through the services provided by the host OS. LibGALS is also suitable as a target for code generation from GALS and synchronous concurrent languages. The experiments demonstrate code size and run-time gains when compared with other approaches to GALS system implementation.

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.