Formal Modeling and Verification of Virtual Community Systems
Elthon Oliveira, Hyggo Almeida, Leandro Silva, Nadia Milena, Frederico Bublitz, Angelo Perkusich
Copyright: © 2008
|Pages: 8
DOI: 10.4018/978-1-59904-885-7.ch081
Abstract
In the last years, virtual community systems (VCS) (Bublitz, Barbosa, & Costa, 2004) have been used as one of the main mechanisms for communication and collaboration among people throughout the world--the people whom use this kind of system compose the socalled virtual community. Several systems providing different features and tools such as forums, e-mails, and videoconference, among others, represent a revolution in the way that people interact with others.
Key Terms in this Chapter
Formal Verification: The process of using formal proofs to demonstrate the consistency (design verification) between a formal specification of a system and a formal security policy model or (implementation verification) between the formal specification and its program implementation.
Model: An abstraction of some characteristic of the business or system, as seen from a particular viewpoint.
CPN/ML: It is a variation of ML functional language used in Coloured Petri Nets.
Component Model: A component model is a specification of patterns for component implementation, documentation, deployment, and usage.
CTL(Computation Tree Logic): It is a type of temporal logic in which different futures are considered.
Temporal Logic: The term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time.
Occurrence Graph: It is a graph in which each node represents a single possible state of the model.