The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Model checking is an automated technique for verifying temporal logic properties of finite state systems. Tarjan's algorithm for detecting Strongly Connected Components (SCCs) is a widely used depth-first search procedure for Automatabased (LTL) model checking. It works on the SCC detection on-the-fly with the composition of transition systems and Büchi Automaton (state space generation), which has...
In this paper we study automated construction of an agent's behavior for a protocol-based multiagent system, where the exact behaviors of the other agents are unknown. This uncertainty makes it challenging to develop an optimal agent behavior that complies with the system protocol, while ensuring achievement of the agent's temporal goals. To solve this problem, we develop an automated method that...
Model checking suffers from the state space explosion problem. Compositional verification techniques such as assume-guarantee reasoning (AGR) have been proposed to alleviate the problem. However, there are at least three challenges in applying AGR. Firstly, given a system M1 ? M2, how do we automatically construct and refine (in the presence of spurious counterexamples) an assumption A2, which must...
In vehicular ad-hoc network, Media AccessControl (MAC) is one of the technologies which determinewhether the information is transferred reliably and timely or not. It is also a key to the quality of service of self organizationnetworks. Some behaviors of the MAC protocol can be estimatedby experiment and simulation. But the main drawback of thesemethods is that the estimation can not be accurate to...
Model checking has been pervasive and successful in finding bugs in hardware and software systems, including real-time and probabilistic systems. Applying model checking to decision making is relative new and has an excellent potential to be compliment to data analytics and other Artificial Intelligent (AI) or Operational Research (OR) based decision making techniques. Our last 8 years research has...
Stochastic model checking is using the verification method of model checking to quantitative verification system model with stochastic behaviours. In recent years, stochastic model checking make a great advancement. In this paper, the high level system model PPN is extended with label, and is used to as the formal model for system with stochastic behaviours; PCTL∗ is selected to as the property specification,...
Game theory has emerged as the powerful semantics for some programming languages and logical systems. At present, it is even used to model checking-based verification process. PCTL (probabilistic computation tree logic) is the extension of CTL (computation tree logic), which can be used for model checking stochastic system models (i.e., stochastic model checking). Using the label-extended PPN (probabilistic...
The main challenge in model checking is the state space explosion. With developments in hardware today, most processors have many cores inside. To leverage on the advances in hardware, we can increase the performance of verifying large models by designing parallel algorithms to run efficiently on multi-core architecture. This work focuses on this problem in the context of Linear Temporal Logic (LTL)...
Hadoop is a popular open source implementation of MapReduce, that has a number of prominent users including Yahoo!, Facebook, and Twitter. Though several works have focused on deploying algorithms on Hadoop MapReduce, research efforts into applying formal methods to prove the correctness of hadoop systems are limited. In this paper we propose a holistic approach to verify the correctness of hadoop...
Model checking has established as an effective method for automatic system analysis and verification. It is making its way into many domains and methodologies. Applying model checking techniques to a new domain (which probably has its own dedicated modeling language) is, however, far from trivial. Translation-based approach works by translating domain specific languages into input languages of a model...
Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal states. Recent research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using different model checking...
Software Architecture plays an essential role in the high level description of a system design. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this paper, we present an automated approach to the modeling and verification of software architecture designs using the Process...
Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal state. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using a newly developed model...
Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is hence interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesize a constraint guaranteeing a correct...
Based on the basic concept of the goal lay of the requirement meta-modeling frame for network software(RGPS-G), this paper advanced a new formal method to guarantee its correctness. The importance of introducing the formal method into RGPS-G was discussed based on the characters of RGPS-G. Theorem proving and model checking had merged in this formal method. Simple formal normative language was used...
In recent years, many Web service composition languages have been proposed. Web service choreography describes collaboration protocols of cooperating Web service participants from a global view. Web service orchestration describes collaboration of the Web services in predefined patterns based on local decision about their interactions with one another at the message/execution level. In this work,...
G-layer of RGPS requirement meta-model is used to refine the general business goals acquired on the basis of the Role layer. A business goal is a high-level and general statement when first proposed. Whether it can be achieved or not depends on the correctness of goal decomposition. Towards these problems, a decomposition model is proposed in this paper. Particularly, with the development of semantic...
UML has become the dominant modeling language in software engineering arena. In order to reduce cost induced by design issues, it is crucial to detect model-level errors in the initial phase of software development. In this paper, we focus on the formal verification of dynamic behavior of UML diagrams. We present an approach to automatically verifying models composed of UML state machines. Our approach...
The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting of a number of nodes that interact with each other to carry out a computation. One essential property of self-stabilizing population protocols is that all nodes must eventually converge to the correct output value, with respect to all possible initial configurations. It has been shown...
High level specification languages like CSP use mathematical objects as abstractions to represent systems and processes. System behaviors are described as process expressions combined with compositional operators, which are associated with elegant algebraic laws for system analysis. Nonetheless, modeling systems with non-trivial data and functional aspects using CSP remains difficult. In this work,...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.