Logs are widely used in various software engineering applications, including debugging, program comprehension, failure prediction, and anomaly detection. Despite their value, the unstructured nature of logs complicates the extraction of meaningful insights. In response, various log parsing techniques leveraging methods like machine learning and pattern recognition have been developed. Nevertheless, existing parsers frequently fail to achieve consistent accuracy, especially when handling complex log formats. To address this challenge, we conduct a comprehensive study to understand the characteristics of log events that lead to parsing errors. Using 16 different log datasets and 8 log parsers, we apply open coding techniques to derive a taxonomy of log event characteristics that contribute to parsing errors. We also examine how different log parsers are impacted by each category in the taxonomy. The resulting taxonomy not only provides insights into the complexity of parsing log data but can also guide the development of advanced parsing tools capable of handling the unique characteristics of diverse log formats.

Space-based navigation systems rely on satellites to operate in orbit and have lifetimes of 10 years or more. Engineers employ Reliability, Availability, and Maintainability (RAM) analysis during the design phase to maximize a satellite's mean time between failures (MTBF). These design parameters help to optimize maintenance plans, enhance overall reliability, and extend the satellite's lifespan. The paper presents a novel approach using concurrent stochastic games (CSG) to model a single satellite with logical and formal specifications of RAM properties in rPATL. We leverage the PRISM-games model checker for quantitative analysis while considering collaborative behaviors between involved players in orbit and on the ground. This CSG-based approach offers a rich design space where actors considered as players involved in satellite maintenance can collaborate and learn optimal strategies.

Logs are essential for the maintenance of large software systems. Software engineers often analyze logs for debugging, root cause analysis , and anomaly detection tasks. Logs, however, are partly structured, making the extraction of useful information from massive log files a challenging task. Recently, many log parsing techniques have been proposed to automatically extract log templates from unstructured log files. These parsers, however, are evaluated using different accuracy metrics. In this paper, we show that these metrics have several drawbacks, making it challenging to understand the strengths and limitations of existing parsers. To address this, we propose a novel accuracy metric, called AML (Accuracy Metric for Log Parsing). AML is a robust accuracy metric that is inspired by research in the field of remote sensing . It is based on measuring omission and commission errors. We use AML to assess the accuracy of 14 log parsing tools applied to the parsing of 16 log datasets. We also show how AML compares to existing accuracy metrics. Our findings demonstrate that AML is a promising accuracy metric for log parsing compared to alternative solutions, which enables a comprehensive evaluation of log parsing tools to help better decision-making in selecting and improving log parsing techniques.

Log parsing is used to extract structures from unstructured log data. It is a key enabler for many software engineering tasks including debugging, fault diagnosis, and anomaly detection. In recent years, we have seen an increase in the number of log parsing techniques and tools. The accuracy of these tools varies significantly. To improve log parsing tools, we need to understand the type of parsing errors they make, which is the purpose of this early research track paper. We achieve this by examining errors of four leading log parsing tools when applied to the parsing of four log datasets generated from various systems. Based on this analysis, we suggest a preliminary classification of log parsing errors, which contains nine categories of errors. We believe that this classification is a good starting point for improving the accuracy of log parsing tools, and also defining better logging practices.

Because of their contribution to the overall reliability assurance process, software logs have become important data assets for the analysis of software systems. Logs are often the only data points that can shed light on how a software system behaves once deployed. Unfortunately, logs are often unstructured data items, hindering viable analysis of their content. There are studies that aim to automatically parse large log files. The primary goal is to create templates from raw log data samples that can later be used to recognize future logs. In this paper, we propose ULP, a Unified Log Parsing tool, which is highly accurate and efficient. ULP combines string matching and local frequency analysis to parse large log files in an efficient manner. First, log events are organized into groups using a text processing method. Frequency analysis is then applied locally to instances of the same group to identify static and dynamic content of log events. When applied to 10 log datasets of the LogPai benchmark, ULP achieves an average accuracy of 89.2%, which outperforms the accuracy of four leading log parsing tools, namely Drain, Logram, SPELL and AEL. Additionally, ULP can parse up to four million log events in less than 3 minutes. ULP is available online as an open source and can be readily used by practitioners and researchers to parse effectively and efficiently large log files so as to support log analysis tasks.

Artificial pancreas enhances the life experience for diabetic patients by allowing them to live normally with their glucose levels controlled automatically with minimal or no intervention. For closed-loop glucose controllers to be approved for clinical practice, they have to prove safety under all potential scenarios. One of the biggest challenges of closed-loop glucose control is to handle the distortion caused by meal intake. This challenge becomes more problematic when taking into account the imperfections and limitations of glucose sensors. In this article, we propose new Proportional-Integral-Derivative (PID)-based control strategies for robust glucose control under varying meal conditions. The proposed approaches aim at counteracting the challenges imposed by the large delays incurred in glucose sensing and insulin action. Statistical model checking was utilized to analyze the performance figures and safety properties as compared with existing closed-loop techniques. The results have shown that one of the proposed approaches provide substantial enhancements towards safe and robust glucose control especially under sensor noise. Where, under a typical relative meal size between 75 and 125 (g/100Kg), the proposed approach can satisfy hypoglycemia safety property for 90% of the patients compared to lower than 50% of the patients for the other investigated techniques. These enhancements can be achieved without additional personalized tuning beyond the standard PID control.

This article addresses the following research question: How to compute no-wait schedules and multipath routings for large-scale time-sensitive networks (TSNs)? TSN must guarantee low latency and fault tolerance. The former requirement is achieved by sending the messages according to a no-wait schedule, whereas the latter is achieved by routing each message through multiple streams of disjoint paths. Computing such schedule and routing is an NP-hard problem. In this article, the aforementioned question is addressed by a three-fold solution: An iterated integer linear programming based scheduling (IIS) technique for scalability; the Degree of Conflict (DoC) between the IIS iterations is minimized by the DoC-aware streams partitioning (DASP) technique, which improves the success rate of the IIS; the fault-tolerance is guaranteed by a DoC-aware multipath routing technique, which integrates the DASP for further improvement in the success rate. Two hundred synthetic test cases are used for performance evaluation. The proposed method scales well, i.e., it handled networks of 21 bridges and 480 messages under 40 min timeout. The success rate of the highly utilized instances raised from 47% by random streams partitioning to 90% by the proposed method.

The reliability of artificial pancreas is crucial for the safety and security of type 1 diabetes. In this paper, new modeling and analysis of the closed-loop glucose control system are proposed to verify and evaluate the performance of control algorithms at the system level. Priced timed automata are used to model the physiological processes, the control algorithm, and the adversary. Two control algorithms are evaluated in normal condition and under replay attack using simulation and model checking. The results show that one of the control algorithms outperforms the other in terms of safety properties. The results also demonstrate the impact of the target attack on the system behavior. The proposed approach provides a new way to evaluate sophisticated control algorithms, security attacks, and attack mitigation techniques.

Many enterprises are adopting deep learning algorithms in their everyday tasks faster than ever. Convolutional Neural Networks (CNNs) in particular are being used widely due to the impressive performance in various application areas. FPGAs, on the other hand, are becoming a promising hardware platform for various deep learning algorithms including CNN. However, optimized and efficient FPGA design requires an expert with hardware design skills. This is particularly a challenge for deep learning practitioners who would like to accelerate their algorithm without worrying about the underlying hardware knowledge required to accomplish that in FPGAs. In this work we are proposing an automated framework, MulMapper, that can generate a functional and synthesized CNN processor hardware IP (using Vivado HLS) for Zynq-based FPGAs, given Caffe-based CNN definition file. We created a dynamic and novel design space utilizing Target Device Resource, Target Core Mode and Target Data Width as design space dimensions. MulMapper explores the design space in these three dimensions and proposes the optimum design points. We tested MulMapper framework on common CNN architectures, LeNet, CNP and CIFAR-10. It has been verified that early-stage MulMapper can lead to synthesis of resource-optimized CNN processor hardware IP that can be used for many regular CNN variants. Comparison with the state-of-the-art shows that architectures generated using MulMapper obtained up to 25-29× DSP48 and 13-20× on-chip memory reduction, with up to 0.35 GOP/sec performance.

Time-Sensitive Networking (TSN) is a set of IEEE standards that are being developed to enable a reliable and real-time communication based on Ethernet technology. It supports Time-Triggered (TT) traffic to allow a low latency as well as deterministic timing behavior. TSN adapts the concept of seamless redundancy to ensure interruption-free fault-resilience. In this paper, our goal is to synthesize a network topology that supports seamless redundant transmission for TT messages. Therefore, we propose a greedy heuristic algorithm for joint topology, routing, and schedule synthesis. The proposed algorithm is capable to generate fault-resilient topology that guarantee feasible routing and scheduling for TT traffic. In particular, the topology is constructed iteratively such that all messages are routed through disjoint paths with a feasible schedule and the network cost is minimized. To achieve this goal, we formulate the topology synthesis problem as iterative path selection problem. Starting from a weighted undirected graph which represents an initial fully-connected network, the cost implied of using each link is mapped as arcs weights in the graph. Then, we adapt Yen's algorithm to iteratively find the minimum-cost paths for the considered messages. The scalability and the efficiency of the proposed approach are demonstrated using 380 synthetic test cases. The results show that the proposed approach is capable of finding fault-resilient topology with up to 50% less cost compared to the typical approach. Moreover, the approach scalability is validated e.g., it handles 24 ECUs with 600 messages problems within an average time of 8 sec.

In this paper, we report experimental results of hybrid system using Hidden Markov Models/Multi-Layer Perceptron (HMM/MLP) model as acoustic model and based on the Fuzzy C-Means (FCM) clustering with optimization with Genetic Algorithm (GA). In this context, we use the result of FCM clustering as initial population of GA, this allows training the GA with a population of empirically generated chromosomes and not randomly initialized. Our results on speech recognition tasks show an increase in the estimates of the posterior probabilities of the correct words after training. We demonstrate the effectiveness of the proposed clustering approach in large-vocabulary speaker-independent continuous speech recognition with regard to the three baseline systems : Discrete HMM, hybrid HMM/MLP with K-Means and FCM clustering.

The vulnerability of VLSI designs to soft errors grows with technology scaling. In order to allow a cost-effective reliability aware design process, it is critical to assess soft error reliability parameters in early design stages. This paper presents a new methodology to estimate digital circuit vulnerability to soft errors of circuits described at Register Transfer Level (RTL). Single Event Upsets (SEUs) propagation through RTL bit-vector operations is modeled and analyzed based on Satisfiability Modulo Theories (SMT). For instance, the bit-vector reduction operators and arithmetic operators were modeled using SMT to include their fault propagation properties. In order to illustrate the practical utilization of our work, we have analyzed different RTL combinational circuits. Experimental results demonstrate that the proposed framework is on average about 4 times faster than other comparable contemporary techniques. Moreover, it provides more accurate and detailed results of the circuit vulnerability allowing a more efficient applicability of fault tolerance techniques.

Ultra-deep sub-micron technologies are more vulnerable to different types of uncertainties. In this paper, we introduce a novel methodology to estimate the vulnerability of sequential circuits to soft errors at gate level. A new probabilistic modeling of SET propagation is proposed, which reduces the complexity of unrolling sequential circuits. This approach enables a multi-cycle error propagation analysis of sequential circuits using only two copies of the circuit combinational part. The proposed probabilistic modeling is based on the proposed backward unrolling approach in conjunction with the proposed formulation of SET propagation into a Satisfability problem by utilizing satisfability modulo theories. Useful information about the SET latency in sequential circuits and the minimum unrolling required to observe the actual behavior of the circuit is generated. These results are then used to estimate the circuit soft error rate. Experimental results demonstrate the effectiveness and applicability of the proposed approach.

The effect of partial volume related to anatomical MRI and functional images limit the diagnostic potential of brain imaging. To remedy for this problem, we propose a fuzzy-genetic brain segmentation scheme for the assessment of white matter, gray matter and cerebrospinal fluid volumes, from brain images of Alzheimer patients from a real database. This clustering process based on Possibilistic C-Means (PCM) algorithm, which allows modeling the degree of relationship between each voxels and a given tissue; and based on fuzzy genetic initialization for the centers of clusters by a Fuzzy C-Means (FCM) algorithm, and for which the result is optimized by genetic process. The visual results show a concordance between the ground truth segmentation and the hybrid algorithm results, which allows efficient tissue classification. The superiority was also proved with the quantitative results of the proposed method in comparison with the both conventional FCM and PCM algorithms.

The cost and complexity involved in the development of critical systems encourage the use of reliability assessment techniques as early in the design cycle as possible. Existing techniques often lack the capacity to perform a comprehensive and exhaustive analysis on complex redundant architectures, leading to less than optimal risk evaluation. This paper addresses these weaknesses by 1) proposing a new probabilistic modeling of Fault Tree gates and their composition as Markov Decision Processes; 2) developing a new formal-based technique to perform an in-depth verification of the system's reliability. This technique makes use of the expressiveness of fault trees and the power of probabilistic model checking in order to investigate the best Triple Modular Redundancy partitioning and configuration of a system. The presented approach greatly improves the overall scalability with respect to other techniques, while also improving the accuracy of the results. For example, we can provide probabilistic failure rates for a chain of 100 redundant components in little over one second.

The progressive shrinking of device sizes in advanced technologies leads to miniaturization and performance improvements. However, ultra-deep sub-micron technologies are more vulnerable to different types of uncertainties, parametric variations, and interference. In this paper, we propose a methodology to model and analyze the behavior of a system in the presence of Single Event Transients (SETs). The problem of SET propagation was modeled as a satisfiability problem using different satisfiability modulo theories. The SET width and timing constraints are formulated as a difference logic constraint satisfaction formulation. This formulation utilizes concepts from static timing analysis to efficiently evaluate the required time and width for the SET to be latched. Next, the proposed model is analyzed using efficient SMT solvers for a set of nonfunctional assertions to investigate SETs propagation. Based on the results of this analysis, new fault observability estimates are computed. These values are then used to compute the soft error rate. Experimental results demonstrate that the proposed SMT approach provides better runtime then contemporary techniques.

This paper presents a hierarchical framework to model, analyze, and estimate digital design vulnerability to soft errors due to Single Event Transients (SETs). A new SET propagation model is proposed. This model simultaneously includes the impact of masking effects, width variation, and re-converging paths by utilizing satisfiability modulo theories. Furthermore, new metrics characterizing the soft error rate of a given design are proposed. Reported results show that the proposed methodology significantly enhances the efficiency of SET analysis in terms of: 1) accuracy as it gives accurate estimates of SET sensitivity based on gates timing extracted from layout. These results provide new insights to combinational designs vulnerability to SETs; 2) speed as it is orders of magnitude faster than contemporary techniques; 3) scalability as it can handle large and complex designs such as 128-bit multipliers, whereas contemporary techniques are unable to handle multipliers larger than 32 bits.

Soft errors due to Single Event Transients (SETs) have become one of the most challenging issues that impact the reliability of modern microelectronic systems at terrestrial altitudes. This is mainly due to the progressive shrinking of device sizes. Traditionally, the analysis of SETs has been carried out by simulations and experimental analysis. However, these techniques are resource hungry and require full details of the design structure and SET characteristics. This paper develops a hierarchical framework for formal analysis of SET propagation by (1) introducing Register Transfer Level (RTL) abstraction and modeling approaches of the underlying behavior of SET propagation using Multiway Decision Graphs (MDGs); and (2) investigating SET propagation conditions at RTL using a formal model checker. In order to illustrate the practical utilization of our work, e have analyzed different RTL combinational designs. Experimental results demonstrate the proposed framework is orders of magnitude faster than other comparable contemporary techniques. Moreover, for the first time, a decision graph based technique s developed to analyze multiplier designs.

SysML/UML activity diagrams are widely used for the modeling and analysis of complex systems and they have become a de-facto standard for software and embedded systems. Previously in our group, we formalized SysML activity diagrams by developing a calculus called New Activity Calculus (NuAC). In this work, we redefine NuAC terms to support code generation for ARM Cortex-M processors and we present an automated SysML activity diagram to RTX (Keil Real-Time Operating System) code generator that uses mapping rules expressed in NuAC. To demonstrate the capability of the developed tool, we use it for scheduling of a JPEG Encoder on an ARM Cortex-M4 device.

Constrained Random Verification (CRV) is becoming the mainstream methodology for the functional verification of complex System on Chip (SoC) designs. In order to achieve verification closure, CRV tools have to produce a large number of solutions, evenly distributed, in the search space. To attain this requirement, we propose a technique which analyzes the solution space by using consistency algorithm and splits the variable's domain into clusters. The proposed technique helps to generate input stimuli which are evenly distributed in search space. The proposed technique has been validated through experimental results. Experimental results show that the proposed methodology guarantees evenly distributed stimuli and improves by about 15% the veriication coverage.

The progressive shrinking of device size in advanced technologies leads to miniaturization and performance improvements. However, ultra-deep sub-micron technologies are more vulnerable to soft errors. Error analysis of a complex system with a sufficiently large sample of vulnerable nodes takes a large amount of time. In this paper we propose RASVAS, a hierarchical statistical method to model, analyze, and estimate the behavior of a system in the presence of Single Event Transients (SETs) modeled at different abstraction levels. Gate level propagation tables are developed to abstract SET propagation conditions and probabilities from gate level models. At RTL, these tables are utilized to model the underlying probabilistic behavior as Markov Decision Process (MDP) models. Experimental results demonstrate that RASVAS is orders of magnitude faster than contemporary techniques and also handle designs as large as 256-bit adders while maintaining accuracy.

Due to shrinking feature sizes and significant reduction in noise margins, as CMOS technologies evolve toward ultra-deep sub-micron, digital circuits have become more susceptible to soft errors. Therefore, researchers have recently reported several approaches to model Single Event Transient (SET) propagation at gate or higher abstraction levels. However, contemporary techniques model only the possibility that SET pulse may be masked electrically, logically, or by time windowing. In this paper, the propagation induced pulse broadening (PIPB) phenomenon is further investigated and a new model which abstracts this phenomenon is proposed. This paper also investigates and abstracts the impact of input patterns and propagation paths on SET pulse width. Through electrical simulations, we validated our analysis.

SRAM-based FPGAs are increasingly popular in the aerospace industry for their field programmability and low cost. However, they suffer from cosmic radiation induced Single Event Upsets (SEUs), commonly known as soft errors. In safety-critical applications, the dependability of the design is a prime concern since failures may have catastrophic consequences. An early analysis of dependability of such safety-critical applications will enable designers to develop a design that meets the high availability and reliability requirements of the DO-254 standard. This paper introduces a novel methodology based on probabilistic model checking, to analyze the dependability properties of safety-critical systems and to suggest required mitigation techniques, such as Triple Modular Redundancy (TMR) or TMR with less frequent scrubs for early design decisions. Starting from a high-level description of a system, a Markov model is constructed from the Control Data Flow Graph (CDFG) expressing the functionality and from failure/mitigation parameters for the targeted FPGAs. Such an exhaustive model captures all the failures and repairs possible in the system within the radiation environment. We present a case study on a benchmark circuit to illustrate the applicability of the proposed approach to demonstrate that a wide range of useful dependability properties can be analyzed using our proposed methodology.

SysML activity diagrams are OMG/INCOSE standard used for modeling and analyzing probabilistic systems. In this paper, we propose a formal verification framework that is based on PRISM probabilistic symbolic model checker to verify the correctness of these diagrams. To this end, we present an efficient algorithm that transforms a composition of SysML activity diagrams to an equivalent probabilistic automata encoded in PRISM input language. To clarify the quality of our verification framework, we formalize both SysML activity diagrams and PRISM input language. Finally, we demonstrate the effectiveness of our approach by presenting a case study.

Abstract In this paper we propose an automatic methodology to verify the soundness of model checking reduction techniques. The idea is to use the consistency of the specifications to verify if the reduced model is faithful to the original one. The user provides the reduction technique, the specification and the system under verification. Then, using Higher Order Logic he verifies automatically if the reduction technique is soundly applied. The method is completely defined in an MDG–HOL special integration platform that combines an automatic high level model checking tool Multiway Decision Graphs (MDGs) within the HOL theorem prover. We provide two case studies, the first one is the reduction using SAT–MDG of an Island Tunnel Controller and the second one is the MDG–HOL assume-guarantee reduction of the Look-Aside Interface. The obtained results of our approach offer a considerable gain in terms of the correctness of heuristics and reduction techniques as applied to commercial model checking, however a small penalty is paid in terms of CPU time and memory usage.

Multi-clock domain circuits with Clock Domain Crossing (CDC) interfaces are emerging as an alternative to circuits with a global clock. CDC interfaces are susceptible to metastability, hence their design is very challenging. This paper presents a hybrid FIFO-asynchronous method for constructing robust CDC interfaces. The proposed design can handle arbitrary clock frequency ratios between the sender and receiver with random phase shifts. The proposed design avoids latency due to synchronizers with the asynchronous protocol modifications. Circuit simulation results confirm the operation and robustness of the design at maximum workloads, and arbitrary frequency ratios, over a temperature range of -50 to 50 degrees Celsius. The interface offers a maximum throughput of 606 million transfers per second without pausing the clock.

Increase in vulnerability to soft errors has affected the reliability of both synchronous and asynchronous circuits implemented in modern deep sub-micron technologies. Hence in such circuits, there is a growing need to identify the soft error glitch propagation possibility at an early stage in the design flow. This paper proposes a new methodology to obtain soft error glitch propagation paths in digital designs (both synchronous and asynchronous). To compute these paths, Multiway Decision Graphs (MDGs) and glitch-propagation sets (GP sets) are utilized in conjunction with Boolean Satisfiability solvers (MiniSat). The applicability of the proposed method is illustrated by implementing ISCAS89 benchmark sequential circuits, 8-bit adders, multipliers, and the Self-timed multiple-group pipeline asynchronous handshake circuits. The proposed SAT based methodology is on average 13 times faster than the best contemporary state-of-the-art techniques exhaustively analyze possible soft error glitch-propagation paths.

Discrete event systems (DES) are a type of dynamic system in which the system behaviour is governed by discrete events occurring asynchronously over time. Most of the logical controllers used now are examples of DES. In this paper we describe the problem faced while modeling a queuing system (which is an example of DES) using constraints in SystemVerilog. The method to overcome the problem is explained and a retrial queuing system is modeled using SystemVerilog. The advantages of modeling DES in SystemVerilog are explained. The performance analysis is done on the SystemVerilog model, compared with another language model called MOSEL.

The standard OMG/INCOSE SysML activity diagrams are behavioral models for specifying and analyzing probabilistic systems. In this paper, we present a formal verification framework for these diagrams that helps to mitigate the state-explosion problem in probabilistic model checking. To do so, we propose to reduce the size of SysML activity diagrams by eliminating and merging precise behaviors. The resulting model is checked using Probabilistic Computation Tree Logic (PCTL) properties. Moreover, we present a calculus for SysML activity diagrams (NuAC) that captures their underlying semantics. In addition, we prove the soundness of our approach by defining a probabilistic weak simulation relation between the semantics of the abstract and the concrete models. This relation is shown to preserve the satisfaction of the PCTL properties. Finally, we demonstrate the effectiveness of our approach on an online shopping system case study.

In this paper, we address the issue of security verification and evaluation of systems at the design level. To this end, we elaborate a practical and formal framework that enables security risk assessment and security requirements verification on systems that are designed using SysML activity diagrams. Our approach is based on probabilistic adversarial interactions between potential attackers and the system design models. These interactions result in a global model that is used to quantify security risks by applying probabilistic model-checking. We rely on a standard catalogue of attack patterns to build a library of attacks' design patterns. To demonstrate the effectiveness of our approach, we apply it on a real-life case study related to the Secure Real Time Streaming Protocol.

Several regular parallel trees have been proposed over the years to optimize logic depth, area, fan-out and interconnect count for logic circuits. In this paper, we propose a comparative study of different parallel prefix trees used in the design of a new end-around carry (EAC) adder targeting FPGA technology. This new adder is based on the fast 128-bit binary floating-point EAC adder which has been implemented in the IBM POWER6 microprocessor's fused multiply-add unit. The parallel prefix tree implemented on the IBM's EAC adder is a Kogge-Stone tree which has been chosen for its high performance and its low power consumption. Our comparative study highlights the main performance differences among fourteen different architecture configurations when targeting an FPGA EAC adder design. We focus on the area requirements and the critical path delay of these designs. Our experimental results show that there is one architecture configuration with the lower area requirement and the higher performance.

The field of remote health monitoring now includes technologies such as home and mobile health monitoring, tele-retinal imaging, tele-radiology, remote cardiac monitoring, video conferencing and sensors for remote diagnosis and treatment to patients. In this regard, implantable wireless body sensor networks (IWBSNs) have recently emerged as an important and growing research area. These implantable sensors are required to be reliable, very small, battery-operated, and capable of collecting data, processing it, and transmitting it wirelessly and efficiently. Since these devices are required to run with limited resources (energy, processing, and memory), their utility protocols (collecting, processing, and communication) should be designed carefully, not only to work reliably but, more importantly, to be resource-efficient. The life time of the embedded batteries associated with these sensor nodes varies from a few days to a few weeks as was described in a previous work by the authors. In this paper, we propose a novel technique which allows the implanted sensor nodes to communicate with a base station located outside the body efficiently by consuming the minimum amount of energy. Our proposed protocol allows the battery to last significantly longer even for years with a gain of up to 100's times of power saving. This will improve the quality of patient life, and reduce risk of infection resulting from frequent chirurgical operations needed to replace such implantable batteries. Also, a new time synchronization algorithm is briefly introduced in this work that is especially applicable to our proposed communication protocol.

In this paper, we are interested in defining a platform for high level model checking using multiway decision graphs (MDGs) within high order logic. The platform is based on the logical formulation of an MDG as a directed formulae (DF). The DF is defined in the HOL theorem prover where the many sorted first-order logic is characterized as a HOL built-in data type. Then, the HOL inference rules are defined to check the well-formedness conditions of any directed formula. Based on this formalization, the MDGs operations are defined as inference rules and consistency and well-formedness proof of each operation is provided. Finally, some experimental results are presented to show the performance of the MDG-HOL platform. The obtained results show that this platform offers a considerable gain in terms of automation without sacrificing CPU time and memory usage.

This paper presents a new traffic management algorithm able to meet the requirements of high speed networks where the speed of ingress traffic can exceeds 10 Gbps. Our newly algorithm, called HRED (high speed RED) is based on the well known algorithm RED (random early detection) algorithm with several enhancements. Unlike other existing enhancements for RED which are found in the literature, our proposed changes leads to an algorithm which outperforms the existing ones in terms of packet drops. The authors present in this paper a series of simulation results demonstrating this fact. Also, the authors developed an efficient heuristic used in the hardware implementation of the algorithm and proved that this heuristic diminishes the response time of the algorithm. The reason for which we claim it's suitability for high speed networks.

Digital communication systems such as modulation-demodulation and M-PSK require the use of carrier synchronization in phase and frequency. This work addresses the implementation and analysis of a digital carrier synchronizer (DCS), which is a phase-locked loop (PLL), realized using digital circuits. This novel methodology highlights implementation promises towards some of the critical issues associated with the design of its analog counterpart, usually known as PLL. The principle function of this DCS is heavily dependent on the numerically controlled oscillator (NCO) and the loop filter (LF). There are various methods to implement NCOs and LFs that are used in the architectural model of DCS. This paper examines the performance of two different NCOs and LFs realization in DCS for modem (modulator-demodulator) application. The methods presented are look up table (LUT) and Xilinx ROM based NCO in one hand, and 1st order and 2nd order based LF. Each has its own merits and de-merits. The paper also developed a mathematical model of DCS for stability analysis. Furthermore, the authors analyzed the performance of this two implementations based on three performance metrics i.e. stability, locking-time and tracking range. From the analysis, Xilinx ROM based NCO with 2nd order LF performs better and are more suited for modem's DCS.

Recent advancement in hardware design urge during a transaction based model as a new intermediate design level. Supporters for the Transaction Level Modeling (TLM) trend claim its efficiency in terms of rapid prototyping and fast simulation incomparison to the classical RTL-based approach. Intuitively, from a verification point of view, faster simulation induces better coverage results. This is driven by two factors: coverage measurement and simulation guidance. In this paper, we propose to use an abstract model of the design, written in the Abstract State Machines Language(AsmL), in order to provide an adequate way for measuring the functional coverage. Then, we use this metric indefining the fitness function of a genetic algorithm proposed to improve the simulation efficiency. Finally, we compare our coverage and simulation results to:(1) random simulation at TLM; and (2) the Specman tool of Verisityat RTL.

In this paper we propose an FPGA implementation of a multi protocol Weighted Fair (WF) queuing algorithm able to handle variable length packets targeted for Packet Over Sonet (POS) interfaces and ideal for the design of hybrid IP/ATM switches. Our contributions is an extension to an existing 4 channel scheduler architecture that combines the Highest Value First scheme and Round Robin scheme, to a modular multi channel scheduler design. The improvement we offer here compared to the previuous implementation is that we have used the existing 4 channel core module to build a higher order WF queuing system without decreasing its overall performance . As a result, our scheduler is general enough to accommodate ATM (UTOPIA Level3/4) , POS Phy Level3 (or PL3 for OC48) as well as POS Phy Level4 (or PL4 for OC192) interfaces.

In this paper, we present a technique to design and verify the look-aside (LA-1) interface standard used in network processors. Our design flow includes several refinements starting from an informal UML specification until getting to an RTL modeled in Verilog. We integrate the verification of the LA-interface in the design flow by considering two intermediate levels: (1) abstract state machines (ASM); and (2) SystemC. The first one serves the verification by model checking of a set of PSL properties, while the second includes a set of assertions to be verified by simulation. To evaluate the performance of our approach, we used the rule-base model checker to verify the same properties; and the OVL library to verify the same assertions.

Receiving large number of data packets at different baud rates and different sizes at gateways in very high-speed network routers may lead to a congestion problem and force them to drop some packets. Several algorithms have been developed to control this problem. A random early detection (RED) algorithm is commonly used. In this work, we present an FPGA implementation of a modified version of RED able to run as fast as 10 Gbps. Furthermore, we discuss three enhancements of the RED algorithm leading a better performance suitable for FPGA implementation.

We propose an FPGA implementation of a multi protocol weighted fair (WF) queuing algorithm able to handle variable length packets targeted for POS interfaces and ideal for the design of hybrid IP/ATM switches. Our contributions are two folds: first, we have combined the Highest Value First scheme and the Round Robin scheme into a single pipelined design able to schedule traffic for 4 channels in parallel. Second, we showed how to build higher order WF queuing system without decreasing the overall performance of our scheduler. As a result, our scheduler is general enough to accommodate ATM (UTOPIA L3/L4) , POS/PL3 (OC48) as well as POS/PL4 (OC192) interfaces.

We study model checking for a first-order linear-time temporal logic. We present the computation model: abstract description of state machines (ASMs), in which data and data operations are described using abstract sort and uninterpreted function symbols. ASMs are suitable for describing Register Transfer level designs. We define a first-order linear-time temporal logic called LMDG which supports the abstract data representations. Both safety and liveness properties can be expressed in LMDG, however, only universal path quantification is possible. Fairness constraints can also be imposed. The property checking algorithms are based on implicit state enumeration of an ASM and implemented using Multiway Decision Graphs.

In order to overcome the limitations of automated tools and the cumbersome proof process of interactive theorem proving, we adopt a hybrid approach for formal hardware verification which uses the strengths of theorem proving (HOL) with powerful mathematical tools such as induction and abstraction, and the advantages of automated tools (MDG) which support equivalence checking and model checking. The MDG system is a decision diagram based verification tool, primarily designed for hardware verification. HOL is a theorem prover built on higher-order logic.

In this paper, we present several techniques for modeling and formal verification of the Fairisle asynchronous transfer mode (ATM) switch fabric using multiway decision graphs (MDGs). MDGs represent a new class of decision graphs which subsumes Bryant's reduced ordered binary decision diagrams (ROBDDs) while accommodating abstract sorts and uninterpreted function symbols. The ATM device we investigated is in use for real applications in the Cambridge University Fairisle network. We modeled and verified the switch fabric at three levels of abstraction: behavior, and register transfer level (RTL) and gate levels. In a first stage, we validated the high-level specification by checking specific safety properties that reflect the behavior of the fabric in its real operating environment. Using the intermediate abstract RTL model, we hierarchically completed the verification of the original gate-level implementation of the switch fabric against the behavioral specification. Since MDGs avoid model explosion induced by data values, this work demonstrates the effectiveness of MDG based verification as an extension of ROBDD-based approaches. All the verifications were carried out automatically in a reasonable amount of CPU time.

Multiway Decision Graphs (MDGs) have been recently proposed as an efficient verification tool for RTL designs based on an efficient representation mechanism. In MDG, a data value is represented by a single variable of abstract sort, and a data operation is represented by an uninterpreted function symbol. In this work we investigate the non-termination problem of MDG-based verification. We present a novel approach to dealing with the problem based on retiming and circuit transformations that preserve the behaviour of the circuit. We demonstrate the effectiveness of our method on the example of the Island Tunnel Controller (ITC).