In this study, the author presents a new efficient algorithm for translating linear temporal logic (LTL) formulas to Büchi automata, which are used by LTL model checkers. The general idea of this algorithm is to generate Büchi automata from LTL formulas, using the principle of alternating automata and keeping only the positive transitions without generating the intermediate generalised automata. The LTL translation is the heart of any LTL model checker, which affects its performance. The translation performance is measured in addition to its speed and the size of the produced Büchi automaton (number of states and number of transitions), by correctness of produced Büchi automaton and its level of determinism. The author will show that this method is different from the others and it is very competitive with the most efficient translators to date.

Shifting market trends towards mobile, Internet of things, and data-centric applications create opportunities for emerging low-power non-volatile memories. The attractive features of spin-torque-transfer magnetic-RAM (STT-MRAM) make it a promising candidate for future on-chip cache memory. Two-bit multiple-level cell (MLC) STT-MRAMs suffer from higher write energy, performance overhead, and lower cell endurance when compared with single-level counterpart. These unwanted effects are mainly due to write operations known as two-step (TT) and hard transitions (HT). Here, the authors offer a solution to tackle write energy problem in MLC STT-MRAM by minimising the number of TT and HT transitions. By analysing real applications, it was observed that specific locations within a cache block undergo much more TT and HT transitions resulting in hot locations when compared with other ones (cold locations). These hot locations are more detrimental to the lifetime and reliability of MRAM device. In this work, the authors propose a simple and intuitive dynamic encoding scheme that eliminates all TT and HT at hot locations, hence reducing energy consumption and improving MLC STT-MRAM lifetime. Results on PARSEC benchmarks demonstrate the effectiveness and scalability of the proposed approach to potentially prolong MLC STT-MRAM lifetime.

Taking into consideration the requirements of real-time embedded systems, the processor scheduler must guarantee a constant scheduling frequency, providing determinism and predictability of tasks execution. The purpose of this study is to implement the nMPRA (multi pipeline register architecture) processor into field-programmable gate array, and to integrate the already existing scheduling methods, thus providing a preemptive schedulability analysis of the proposed architecture based on the pipeline assembly line and hardware scheduler. This study describes a hardware implementation of the real-time scheduler named nHSE (hardware scheduler engine for n tasks) and presents the results obtained using the appropriate schedulability methods used in real-time environments. The scheduling and task switch operations are the main source of non-determinism, being successfully dealt with real-time nMPRA concept, in order to improve the system's functionality. Some mechanisms used for synchronisation and inter-task communication are also taken into consideration.

As cyber physical system (CPS) is often used in safety critical areas, dependability of the system is an important issue that needs to be analysed. Any failure on the components of the CPS could result in a degradation of the physical state, which then causes major harm to life and/or property. Since the concept of dependence leads to that of trust, the subsystems of the CPS should be dependable to each other to deliver the requested services as specified without failing during its operation. In this study, the authors apply Markov chain to model and analyse the component dependability of CPSs and propose the recovery techniques to guarantee a high level of dependability so as to take care of assuring the continuity of system operation.