Titlebook: Structured Object-Oriented Formal Language and Method; 5th International Wo Shaoying Liu,Zhenhua Duan Conference proceedings 2016 Springer

暴露他抗议

砍伐

A GUI-Aided Approach to Formal Specification Constructionign. By this approach, a GUI prototyping for the system is first carried out based on an informal requirements specification with the aim of improving the informal specification and then a formal design specification is constructed to precisely define the system architecture and functionality. We de

宇宙你

Automatic Generation of Specification-Based Test Cases by Applying Genetic Algorithms in Reinforcemem which assuming the existence of a bug related to a global variable are reported. For software development based on formal specifications, a number of methods for the automatic generation of test cases have previously been proposed. However, most of those methods are for testing whether or not the

Creatinine-Test

Fault Localization of Timed Automata Using Maximum Satisfiabilitylthough these tools are effective to detect faulty behavior, localizing root causes of faulty timed automata requires a costly manual task of studying counter-examples. This paper presents an automatic fault localization problem. The proposed approach follows the Reiter’s model-based diagnosis theor

OGLE

Automated Program Debugging for Multiple Bugs Based on Semantic AnalysisMPS)[.], which try to find a successful execution trace by switching outcomes of multiple predicates. Substantively, BMPS focuses on the program faults which are caused by control flow. However, this kind of faults represent only a small fraction. In this paper, we present an algorithm combining BMP

缺陷

彩色的蜡笔

口味

A Case Study: SOFL + Model Checking for OSEK/VDX Applicationand more automotive applications have been developed based on OSEK/VDX OS. As the continuously increasing complexity in the development of the applications, how to efficiently develop an application is becoming a challenge. A primary problem is the requirement specification may not be accurately and

mortgage

On Reachability Analysis of Updatable Timed Automata with One Updatable Clockbility of general UTAs is undecidable, by regarding a pair of updatable clocks as counters updatable with incrementation and decrementation operations. This paper investigates the model of subclass of UTAs by restricting the number of updateable clocks. It is shown that the reachability of . under d

narcissism

Research on Formal Development of Non-recursive Algorithms of Graph Searcho formally develop two non-recursive graph search algorithms, depth-first search and breadth-first search. This is a very challenge task because non-recursive graph search algorithms have low computing complexity with high logic complexity comparing with recursive graph search algorithms. The formal