Network simulators, which implement network protocols under some simulated conditions. have been widely used to analyze the feasibility of network protocols. Conformance testing of the simulator against the protocol i...
详细信息
ISBN:
(纸本)9783642021374
Network simulators, which implement network protocols under some simulated conditions. have been widely used to analyze the feasibility of network protocols. Conformance testing of the simulator against the protocol is a very important task ill the community of However. many current, conformance testing, method face a problem of finding a systematic mechanism to verify the tests outputs. this paper proposes to use all innovative testing approach, metamorphic testing (MT), to alleviate such a problem. We select one adhoc on-demand distance vector (AODV) simulator for study, and test its conformance against the AODV protocol by the MT technique. through our, experiments, we illustrate the applicability of NIT ill the protocol conformance testing, confirm the reliability of the selected AODV simulator and demonstrate the cost-effectiveness of NIT using the mutation analysis technique.
the proceedings contain 19 papers. the topics discussed include: the Orc programming language;keep it small, keep it real: efficient run-time verification of web service compositions;approximated context-sensitive ana...
ISBN:
(纸本)3642021379
the proceedings contain 19 papers. the topics discussed include: the Orc programming language;keep it small, keep it real: efficient run-time verification of web service compositions;approximated context-sensitive analysis for parameterized verification;verification of parameterized systems with combinations of abstract domains;on model-checking optimistic replication algorithms;a software platform for timed mobility and timed interaction;modeling, validation, and verification of PCEP using the IF language;distinguing non-deterministic timed finite state machines;system model-based definition of modeling language semantics;typing component-based communication systems;epistemic logic for the applied Pi calculus;on process-algebraic proof methods for fault tolerant distributedsystems;using first-order logic to reason about submodule construction;a model-checking approach for service component architectures;and dynamic symbolic execution of distributed concurrent objects.
the proceedings contain 19 papers. the special focus in this conference is on Model Checking, Rewriting Logic, Components and Algebraic Calculi. the topics include: Asynchronous session types and progress for object o...
ISBN:
(纸本)3540729194
the proceedings contain 19 papers. the special focus in this conference is on Model Checking, Rewriting Logic, Components and Algebraic Calculi. the topics include: Asynchronous session types and progress for object oriented languages;a formal method for object-oriented systems;verifying distributed, event-based middleware applications using domain-specific software model checking;model checking of extended OCL constraints on UML models in SOCLe;analysis of UML activities using dynamic meta modeling;distributed applications implemented in Maude with parameterized skeletons;on formal analysis of OO languages using rewriting logic;formal modeling and analysis of the OGDC wireless sensor network algorithm in real-time Maude;adaptation of open component-basedsystems;a representation-independent behavioral semantics for object-oriented components;a mechanized model of the theory of objects;refactoring object-oriented specifications with data and processes;a sound and complete shared-variable concurrency model for multi-threaded java programs;performance-oriented comparison of web services via client-specific testing preorders;a probabilistic formal analysis approach to cross layer optimization in distributed embedded systems and on resource-sensitive timed component connectors.
the proceedings contain 19 papers. the topics discussed include: asynchronous session types and progress for object oriented languages;model checking of extended OCL constraints on UML models in SOCLe;analysis of UML ...
详细信息
ISBN:
(纸本)3540729194
the proceedings contain 19 papers. the topics discussed include: asynchronous session types and progress for object oriented languages;model checking of extended OCL constraints on UML models in SOCLe;analysis of UML activities using dynamic meta modeling;distributed applications implemented in Maude with parameterized skeletons;formal modeling and analysis of the OGDC wireless sensor network algorithm in real-time Maude;adaptation of open component-basedsystems;a representation-independent behavioral semantics for object-oriented components;a formal language for electronic contracts;a mechanized model of the theory of objects;a refinement method for java programs;refractoring object-oriented specifications with data and processes;a sound and complete shared-variable concurrency model for multi-threaded Java Programs;and performance-oriented comparison of web services via client-specific testing preorders.
this paper presents a minimal and complete set of structural refactoring rules for the object-Z specification language that allow for the derivation of arbitrary object-oriented architectures. the rules are equivalenc...
详细信息
ISBN:
(纸本)9783540688624
this paper presents a minimal and complete set of structural refactoring rules for the object-Z specification language that allow for the derivation of arbitrary object-oriented architectures. the rules are equivalence preserving and work in concert with existing class refinement theory, so that any design derived using the rule set can be shown to be equivalent to, or a refinement of, the original specification.
Concurrent programming in object-oriented languages is a notoriously difficult task. We propose coboxes - a novel language concept which combines and generalizes active objects and techniques for heap structuring. CoB...
详细信息
ISBN:
(纸本)9783540688624
Concurrent programming in object-oriented languages is a notoriously difficult task. We propose coboxes - a novel language concept which combines and generalizes active objects and techniques for heap structuring. CoBoxes realize a data-centric approach that guarantees mutual-exclusion for groups of objects. this is important for more complex data structures with invariants ranging over several objects. CoBoxes support multiple entry objects, several cooperating tasks in a cobox, and nesting of coboxes for composition and internal parallelism. Communication between coboxes is handled by asynchronous method calls with futures, which is in particular suitable for distributed programming. In this paper, we explain how aspects of concurrent programming can be solved by coboxes. We develop a core language for coboxes and present a formal operational semantics for this language.
Runtime security policy enforcement systems are crucial to limit the risks associated with running untrustworthy (malicious or buggy) code. the inlined reference monitor approach to policy enforcement, pioneered by Er...
详细信息
ISBN:
(纸本)9783540688624
Runtime security policy enforcement systems are crucial to limit the risks associated with running untrustworthy (malicious or buggy) code. the inlined reference monitor approach to policy enforcement, pioneered by Erlingsson and Schneider, implements runtime enforcement through program rewriting: security checks are inserted inside untrusted programs. Ensuring complete mediation - the guarantee that every security-relevant event is actually intercepted by the monitor - is non-trivial when the program rewriter operates on an object-oriented intermediate language with state-of-the-art features such as virtual methods and delegates. this paper proposes a caller-side rewriting algorithm for MSIL - the bytecode of the NET virtual machine - where security checks are inserted around calls to security-relevant methods. We prove that this algorithm achieves sound and complete mediation and transparency for a simplified model of MSIL, and we report on our experiences withthe implementation of the algorithm for full MSIL.
In this work, novel symbolic step encodings of the transition relation for objectbased communicating state machines are presented. this class of systems is tailored to capture the essential data manipulation features...
详细信息
ISBN:
(纸本)9783540688624
In this work, novel symbolic step encodings of the transition relation for objectbased communicating state machines are presented. this class of systems is tailored to capture the essential data manipulation features of UML state machines when enriched with a Java-like object oriented action language. the main contribution of the work is the generalization of the there exists-step semantics approach, which Rintanen has used for improving the efficiency of SAT based AI planning, to a much more complex class of systems. Furthermore, the approach is extended to employ a dynamic notion of independence. To evaluate the encodings, UML state machine models are automatically translated into NuSMV models and then, symbolically model checked with NuSMV. Especially in bounded model checking (BMC), the there exists-step semantics often significantly outperforms the traditional interleaving semantics without any substantial blowup in the BMC encoding as a SAT formula.
Reasoning about object-oriented programs is hard, due to aliasing, dynamic binding and the need for data abstraction and framing. Reasoning about concurrent object-oriented programs is even harder, since in general in...
详细信息
ISBN:
(纸本)9783540688624
Reasoning about object-oriented programs is hard, due to aliasing, dynamic binding and the need for data abstraction and framing. Reasoning about concurrent object-oriented programs is even harder, since in general interference by other threads has to be taken into account at each program point. In this paper, we propose an approach to the automatic verification of concurrent Java-like programs. the cornerstone of the approach is a programming model, a set of rules, which limits thread inference to synchronization points such that one can reason sequentially about most code. In particular, programs conforming to the programming model are guaranteed to be data race free. Compared to previous incarnations of the programming model, our approach is more flexible in describing the set of memory locations protected by an object's lock. In addition, we combine the model with an approach for data abstraction and framing based on dynamic frames. To the best of our knowledge, this is the first paper combining dynamic frames and concurrency. We implemented the approach in a tool, called VeriCool, and used it to verify several small concurrent programs.
暂无评论