Formal Modeling and Verification of Virtual Community Systems
Elthon Oliveira (Federal University of Alagoas, Campus Arapiraca, Brazil), Hyggo Almeida (Federal University of Campina Grande, Brazil), Leandro Silva (Federal University of Campina Grande, Brazil), Nadia Milena (Federal University of Campina Grande, Brazil), Frederico Bublitz (Federal University of Campina Grande, Brazil) and Angelo Perkusich (Federal University of Campina Grande, Brazil)
Copyright: © 2008
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.