scholarly journals DICER 2.0: A New Model Checker for Data-Flow Errors of Concurrent Software Systems

Mathematics ◽  
2021 ◽  
Vol 9 (9) ◽  
pp. 966
Author(s):  
Dongming Xiang ◽  
Fang Zhao ◽  
Yaping Liu
Keyword(s):  
Petri Net ◽  
Data Flow ◽  
Computing Methods ◽  
Software Systems ◽  
Model Checker ◽  
Concurrent Software ◽  
New Model ◽  
Data Flows ◽  
System Properties ◽  
Analyze Data

Petri nets are widely used to model concurrent software systems. Currently, there are many different kinds of Petri net tools that can analyze system properties such as deadlocks, reachability and liveness. However, most tools are not suitable to analyze data-flow errors of concurrent systems because they do not formalize data information and lack efficient computing methods for analyzing data-flows. Especially when a concurrent system has so many concurrent data operations, these Petri net tools easily suffer from the state–space explosion problem and pseudo-states. To alleviate these problems, we develop a new model checker DICER 2.0. By using this tool, we can model the control-flows and data-flows of concurrent software systems. Moreover, the errors of data inconsistency can be detected based on the unfolding techniques, and some model-checking can be done via the guard-driven reachability graph (GRG). Furthermore, some case studies and experiments are done to show the effectiveness and advantage of our tool.

Digital Uncanny

2019 ◽  
Author(s):  
Kriss Ravetto-Biagioli
Keyword(s):  
Feedback Loop ◽  
Aesthetic Experience ◽  
Software Systems ◽  
Repressed Memories ◽  
Experimental Art ◽  
The Uncanny ◽  
Art Works ◽  
Data Flows ◽  
Human Gestures ◽  
New Type

We are confronted with a new type of uncanny experience, an uncanny evoked by parallel processing, aggregate data, and cloud-computing. The digital uncanny does not erase the uncanny feeling we experience as déjà vu or when confronted with robots that are too lifelike. Today’s uncanny refers to how nonhuman devices (surveillance technologies, algorithms, feedback, and data flows) anticipate human gestures, emotions, actions, and interactions, intimating we are machines and our behavior is predicable because we are machinic. It adds another dimension to those feelings we get when we question whether our responses are subjective or automated—automated as in reducing one’s subjectivity to patterns of data and using those patterns to present objects or ideas that would then elicit one’s genuinely subjective—yet effectively preset—response. This anticipation of our responses is a feedback loop we have produced by designing software that studies our traces, inputs, and moves. Digital Uncanny explores how digital technologies, particularly software systems working through massive amounts of data, are transforming the meaning of the uncanny that Freud tied to a return of repressed memories, desires, and experiences to their anticipation. Through a close reading of interactive and experimental art works of Rafael Lozano-Hemmer, Bill Viola, Simon Biggs, Sue Hawksley, and Garth Paine, this book is designed to explore how the digital uncanny unsettles and estranges concepts of “self,” “affect,” “feedback,” and “aesthetic experience,” forcing us to reflect on our relationship with computational media and our relationship to others and our experience of the world.

scholarly journals A Survey of Recent Trends in Testing Concurrent Software Systems

2018 ◽  
Vol 44 (8) ◽  
pp. 747-783 ◽  
Author(s):  
Francesco Adalberto Bianchi ◽  
Alessandro Margara ◽  
Mauro Pezze
Keyword(s):  
Software Systems ◽  
Concurrent Software ◽  
Recent Trends

VERIFICATION OF DATAFLOW SCHEDULING

2008 ◽  
Vol 18 (06) ◽  
pp. 737-758
Author(s):  
TSUNG-HSI CHIANG ◽  
LAN-RONG DUNG
Keyword(s):  
Formal Verification ◽  
Petri Net ◽  
Register Transfer Level ◽  
Functional Verification ◽  
Model Checker ◽  
Symbolic Model ◽  
Verification Method ◽  
Level Design ◽  
High Level ◽  
Design Scheduling

This paper presents the formal verification method for high-level synthesis (HLS) to detect design errors of dataflow algorithms by using Petri Net (PN) and symbolic-model-verifier (SMV) techniques. Formal verification in high-level design means architecture verification, which is different from functional verification in register transfer level (RTL). Generally, dataflow algorithms need algorithmic transformations to achieve optimal goals and also need design scheduling to allocate processor resources before mapping on a silicon. However, algorithmic transformations and design scheduling are error-prone. In order to detect high-level faults, high-level verification is applied to verify the synthesis results in HLS. Instead of applying Boolean algebra in traditional verification, this paper adopts both Petri Net theory and SMV model checker to verify the correctness of the synthesis results of the high-level dataflow designs. In the proposed hybrid verification method, a high-level design or DUV (design-under-verification) is first transformed into a Petri Net model. Then, Petri Net theory is applied to check the correctness of its algorithmic transformations of HLS, and the SMV model checker is used to verify the correctness of the design scheduling. We presented two approaches to realize the proposed verification method and concluded the best one who outperforms the other in terms of processing speed and resource usage.

Sign in / Sign up

Export Citation Format

Share Document