BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Sofiene Tahar

Sofiene Tahar contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
eess.SPeess.SYLogic in Computer ScienceSystems and ControlEmerging TechnologiesFormal Languages and Automata Theoryphysics.optics

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
6works
0followers
7topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

6 published item(s)

preprint2021arXiv

Formal FT-based Cause-Consequence Reliability Analysis using Theorem Proving

Cause-consequence Diagram (CCD) is widely used as a deductive safety analysis technique for decision-making at the critical-system design stage. This approach models the causes of subsystem failures in a highly-critical system and their potential consequences using Fault Tree (FT) and Event Tree (ET) methods, which are well-known dependability modeling techniques. Paper-and-pencil-based approaches and simulation tools, such as the Monte-Carlo approach, are commonly used to carry out CCD analysis, but lack the ability to rigorously verify essential system reliability properties. In this work, we propose to use formal techniques based on theorem proving for the formal modeling and step-analysis of CCDs to overcome the inaccuracies of the simulation-based analysis and the error-proneness of informal reasoning by mathematical proofs. In particular, we use the HOL4 theorem prover, which is a computer-based mathematical reasoning tool. To this end, we developed a formalization of CCDs in Higher-Order Logic (HOL), based on the algebraic approach, using HOL4. We demonstrate the practical effectiveness of the proposed CCD formalization by performing the formal reliability analysis of the IEEE 39-bus electrical power network. Also, we formally determine the Forced Outage Rate (FOR) of the power generation units and the network reliability index, i.e., System Average Interruption Duration Index (SAIDI). To assess the accuracy of our proposed approach, we compare our results with those obtained with MATLAB Monte-Carlo Simulation (MCS) as well as other state-of-the-art approaches for subsystem-level reliability analysis.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Optical Stochastic Computing Architectures Using Photonic Crystal Nanocavities

Stochastic computing allows a drastic reduction in hardware complexity using serial processing of bit streams. While the induced high computing latency can be overcome using integrated optics technology, the design of realistic optical stochastic computing architectures calls for energy efficient switching devices. Photonics Crystal (PhC) nanocavities are $μm^2$ scale devices offering 100fJ switching operation under picoseconds-scale switching speed. Fabrication process allows controlling the Quality factor of each nanocavity resonance, leading to opportunities to implement architectures involving cascaded gates and multi-wavelength signaling. In this report, we investigate the design of cascaded gates architecture using nanocavities in the context of stochastic computing. We propose a transmission model considering key nanocavity device parameters, such as Quality factors, resonance wavelength and switching efficiency. The model is calibrated with experimental measurements. We propose the design of XOR gate and multiplexer. We illustrate the use of the gates to design an edge detection filter. System-level exploration of laser power, bit-stream length and bit-error rate is carried out for the processing of gray-scale images. The results show that the proposed architecture leads to 8.5nJ/pixel energy consumption and 512ns/pixel processing time.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A Formally Verified HOL4 Algebra for Event Trees

Event Tree (ET) analysis is widely used as a forward deductive safety analysis technique for decision-making at the critical-system design stage. ET is a schematic diagram representing all possible operating states and external events in a system so that one of these possible scenarios can occur. In this report, we propose to use the HOL4 theorem prover for the formal modeling and step-analysis of ET diagrams. To this end, we developed a formalization of ETs in higher-order logic, which is based on a generic list datatype that can: (i) construct an arbitrary level of ET diagrams; (ii) reduce the irrelevant ET branches; (iii) partition ET paths; and (iv) perform the probabilistic analysis based on the occurrence of certain events. For illustration purposes, we conduct the formal ET stepwise analysis of an electrical power grid and also determine its System Average Interruption Frequency Index (SAIFI), which is an important indicator for system reliability.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

ETMA: A New Software for Event Tree Analysis with Application to Power Protection

Event Tree (ET) analysis is a widely used forward deductive safety analysis technique for decision-making at a system design stage. Existing ET tools usually provide Graphical Users Interfaces (GUI) for users to manually draw system-level ET diagrams, which consist of nodes and branches, describing all possible success and failure scenarios. However, these tools do not include some important ET analysis steps, e.g., the automatic generation and reduction of a complete system ET diagram. In this paper, we present a new Event Trees Modeling and Analysis (ETMA) tool to facilitate users to conduct a complete ET analysis of a given system. Some key features of ETMA include: (i) automatic construction of a complete ET model of real-world systems; (ii) deletion/reduction of unnecessary ET nodes and branches; (iii) partitioning of ET paths; and (iv) probabilistic analysis of the occurrence of a certain event. For illustration purposes, we utilize our ETMA tool to conduct the ET analysis of a protective fault trip circuit in power grid transmission lines. We also compared the ETMA results with Isograph, which is a well-known commercial tool for ET analysis.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Formal Verification of Cyber-Physical Systems using Theorem Proving (Invited Paper)

Due to major breakthroughs in software and engineering technologies, embedded systems are increasingly being utilized in areas ranging from aerospace and next-generation transportation systems, to smart grid and smart cities, to health care systems, and broadly speaking to what is known as Cyber-Physical Systems (CPS). A CPS is primarily composed of several electronic, communication and controller modules and some actuators and sensors. The mix of heterogeneous underlying smart technologies poses a number of technical challenges to the design and more severely to the verification of such complex infrastructure. In fact, a CPS shall adhere to strict safety, reliability, performance and security requirements, where one needs to capture both physical and random aspects of the various CPS modules and then analyze their interrelationship across interlinked continuous and discrete dynamics. Often times however, system bugs remain uncaught during the analysis and in turn cause unwanted scenarios that may have serious consequences in safety-critical applications. In this paper, we introduce some of the challenges surrounding the design and verification of contemporary CPS with the advent of smart technologies. In particular, we survey recent developments in the use of theorem proving, a formal method, for the modeling, analysis and verification of CPS, and overview some real world CPS case studies from the automotive, avionics and healthtech domains from system level to physical components.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Machine Learning-Based Self-Compensating Approximate Computing

Dedicated hardware accelerators are suitable for parallel computational tasks. Moreover, they have the tendency to accept inexact results. These hardware accelerators are extensively used in image processing and computer vision applications, e.g., to process the dense 3-D maps required for self-driving cars. Such error-tolerant hardware accelerators can be designed approximately for reduced power consumption and/or processing time. However, since for some inputs the output errors may reach unacceptable levels, the main challenge is to \textit{enhance the accuracy} of the results of approximate accelerators and keep the error magnitude within an allowed range. Towards this goal, in this paper, we propose a novel machine learning-based self-compensating approximate accelerators for energy efficient systems. The proposed error \textit{compensation module}, which is integrated within the architecture of approximate hardware accelerators, efficiently reduces the accumulated error at its output. It utilizes \textit{lightweight supervised machine learning techniques, i.e., decision tree}, to capture input dependency of the error. We consider image blending application in multiplication mode to demonstrate a practical application of self-compensating approximate computing. Simulation results show that the proposed design of self-compensating approximate accelerator can achieve about 9\% accuracy enhancement, with negligible overhead in other performance measures, i.e., power, area, delay and energy.

0 citations0 reviewsNo code linkedOpen access