We consider a model for representing infinite-state and parameterized systems, in which states are represented as strings over a finite alphabet. Actions are transformations on strings, in which the change can be char...
详细信息
ISBN:
(纸本)3540672826
We consider a model for representing infinite-state and parameterized systems, in which states are represented as strings over a finite alphabet. Actions are transformations on strings, in which the change can be characterised by an arbitrary finite-state transducer. this program model is able to represent programs operating on a variety of data structures, such as queues, stacks, integers, and systems with a parameterized linear topology. the main contribution of this paper is an effective derivation of a general and powerful transitive closure operation for this model. the transitive closure of an action represents the effect of executing the action an arbitrary number of times. For example, the transitive closure of an action which transmits a single message to a buffer will be an action which sends an arbitrarily long sequence of messages to the buffer. Using this transitive closure operation, we show how to model and automatically verify safety properties for several types of infinite-state and parameterized systems.
A major problem in model-checking timed systems is the huge memory requirement. In this paper, we study the memory-block traversal problems of using standard operating systems in exploring the state-space of timed aut...
详细信息
ISBN:
(纸本)3540672826
A major problem in model-checking timed systems is the huge memory requirement. In this paper, we study the memory-block traversal problems of using standard operating systems in exploring the state-space of timed automata. We report a case study which demonstrates that deallocating memory blocks (i.e. memory-block traversal) using standard memory management routines is extremely time-consuming. the phenomenon is demonstrated in a number of experiments by installing the UPPAAL tool on Windows95, SunOS 5 and Linux. It seems that the problem should be solved by implementing a memory manager for the model-checker, which is a troublesome task as it is involved in the underlining hardware and operating system. We present an alternative technique that allows the model-checker to control the memory-block traversal strategies of the operating systems without implementing an independent memory manager. the technique is implemented in the UPPAAL model-checker. Our experiments demonstrate that it results in significant improvement on the performance of UPPAAL. For example, it reduces the memory deallocation time in checking a start-up synchronisation protocol on Linux from 7 days to about 1 hour. We show that the technique can also be applied in speeding up re-traversals of explored state-space.
the proceedings contain 34 papers. the special focus in this conference is on Knowledge Modelling Languages and tools. the topics include: OIL in a nutshell;combining interoperability and flexibility;the MOKA modellin...
ISBN:
(纸本)3540411194
the proceedings contain 34 papers. the special focus in this conference is on Knowledge Modelling Languages and tools. the topics include: OIL in a nutshell;combining interoperability and flexibility;the MOKA modelling language;a modelling language to build a formal ontology in either description logics or conceptual graphs;a roadmap to ontology specification languages;a formal ontology of properties;construction and deployment of a plant ontology;the role of ontologies for an effective and unambiguous dissemination of clinical guidelines;supporting inheritance mechanisms in ontology representation;conflict resolution in the collaborative design of terminological knowledge bases;a methodology based on corpus analysis;an iterative algorithm to organize relational knowledge;informed selection of training examples for knowledge refinement;experiences with a generic refinement toolkit;chinese encyclopaedias and balinese cockfights;integrating textual knowledge and formal knowledge for improving traceability;knowledge management by reusing experience;integrating knowledge-based configuration systems by sharing functional architectures;the nature of knowledge in an abductive event calculus planner;adapting tableaux for classification;conceptual information systems discussed through an IT-security tool;translations of ripple down rules into logic formalisms;generalising ripple-down rules;monitoring knowledge acquisition instead of evaluating knowledge bases and a quantitative analysis for the robustness of knowledge-based systems.
作者：
Wohed, PStockholm Univ
Royal Inst Technol Dept Informat & Syst Sci S-16440 Kista Sweden
Reuse of already existing resources and solutions has always been a strategy for reducing the costs in the information systems development process. construction and organization of small pieces of reusable solutions, ...
详细信息
ISBN:
(纸本)3540676309
Reuse of already existing resources and solutions has always been a strategy for reducing the costs in the information systems development process. construction and organization of small pieces of reusable solutions, also called patterns, in libraries for reuse support, has taken a central place within research during the last years. In this paper, a methodology for collecting conceptual patterns and a navigation structure for suggesting the most suitable one during the information systemsanalysis process are suggested. the study has, so far, been carried out on one domain only, but it provides a theoretical background for research on other domains as well.
the proceedings contain 31 papers. the special focus in this conference is on Real-Time, Compositionality and Abstraction. the topics include: Modeling for mere mortals;scheduling system verification;a period assignme...
ISBN:
(纸本)3540657037
the proceedings contain 31 papers. the special focus in this conference is on Real-Time, Compositionality and Abstraction. the topics include: Modeling for mere mortals;scheduling system verification;a period assignment algorithm for real-time system design;analyzing stochastic fixed-priority real-time systems;timed diagnostics for reachability properties;fighting livelock in the i-protocol;proving the soundness of a java bytecode verifier specification in isabelle/HOL;automated fast-track reconfiguration of group communication systems;specifications and proofs for ensemble layers;an automated analysis of ping-pong interactions in e-mail services;automatic verification of cryptographic protocols through compositional analysis techniques;verification of hierarchical state/event systems using reusability and compositionality;on proving safety properties by integrating static analysis, theorem proving and abstraction;symbolic model checking without BDDs;symbolic verification of lossy channel systems;model checking in CLP;using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe petri nets finite state verification for the asynchronous pi-calculus;process algebra in PVS;on the benefits of using the up to techniques for bisimulation verification;computing strong/weak bisimulation equivalences and observation congruence for value-passing processes;hardware testing using a communication protocol conformance testing tool;a light-weight framework for hardware verification;an easily extensible toolset for tabular mathematical expressions;from DFA-frameworks to DFA-generators;a theorem prover-based analysis tool for object-oriented databases and an environment for embedded system design and analysis.
Configuration problems are a thriving application area for declarative knowledge representation that experiences a constant increase in size and complexity of knowledge bases. However, today's configurators are de...
详细信息
ISBN:
(纸本)3540411194
Configuration problems are a thriving application area for declarative knowledge representation that experiences a constant increase in size and complexity of knowledge bases. However, today's configurators are designed for solving local configuration problems not providing any distributed configuration problem solving functionality. Consequently the challenges for the construction of configuration systems are the integrated support of configuration knowledge base development and maintenance and the integration of methods that enable distributed configuration problem solving. In this paper we show how to employ a standard design language (Unified Modeling Language - UML) for the construction of configuration knowledge bases (component structure and functional architecture) and automatically translate the resulting models into an executable logic representation which can further be exploited for calculating distributed configurations. Functional architectures are shared among cooperating configuration systems serving as basis for the exchange of requirements between those systems. An example for configuring cars shows the whole process from the design of the configuration model to distributed configuration problem solving.
the proceedings contain 33 papers. the special focus in this conference is on Advanced Information systems Engineering. the topics include: Towards extensible information brokers based on xml;advertising database capa...
ISBN:
(纸本)9783540676300
the proceedings contain 33 papers. the special focus in this conference is on Advanced Information systems Engineering. the topics include: Towards extensible information brokers based on xml;advertising database capabilities for information sharing;extending a conceptual modelling approach to web application design;efficient distributed workflow management based on variable server assignments;a logical framework for exception handling in ADOME workflow management system;controlled flexibility in workflow management;a formal model for business process modeling and design;conceptual patterns for reuse in information systemsanalysis;evaluating a pattern approach as an aid for the development of organisational knowledge;design principles for application integration;modeling and composing service-based and reference process-based multi-enterprise processes;an awareness engine for increasing product awareness in distributed development projects;how culture might impact on the implementation of enterprise resource planning packages;capture and dissemination of experience about the construction of engineering processes;practical reuse measurement in ERP requirements engineering;a framework for the evolution of temporal conceptual schemas of information systems;distance measures for information system reengineering;a tool for integrating UML and Z specifications;on structured workflow modelling;a model for data warehouse operational processes;temporally faithful execution of business transactions;modelling and optimisation issues for multidimensional databases;managing the software process in the middle of rapid growth and the impacts of electronic commerce in the automobile industry.
there is a growing trend to integrate theorem proving systems with specialized decision procedures and model checking systems. the proving capabilities of the PVS theorem prover, for example, have been improved consid...
ISBN:
(纸本)3540677704
there is a growing trend to integrate theorem proving systems with specialized decision procedures and model checking systems. the proving capabilities of the PVS theorem prover, for example, have been improved considerably by extending it with new proof tactics based on a BDD package, a μ-calculus model-checker [4], and a polyhedral library. In this way, a theorem proving system like PVS provides a common front-end and specification language for a variety of specialized tools. this makes it possible to use a whole arsenal of verification and validation methods in a seamless way, combine them using a strategy language, and provide development chain analysis.
Conformance testing is still the main industrial validation technique for telecommunication protocols. the automatic construction of test cases based on the model approach is hindered by the state explosion problem. O...
详细信息
the introduction of symbolic model checking using Binary Decision Diagrams (BDDs) has led to a substantial extension of the class of systemsthat can be algorithmically verified. Although BDDs have played a crucial ro...
详细信息
暂无评论