Model checking is an algorithmic verification technique that checks automatically whether a given finite
state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state s...Model checking is an algorithmic verification technique that checks automatically whether a given finite
state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space
explosion problem. In this paper, several important approaches have been proposed for dealing with the state
explosion problem. Such approaches are symbolic, abstraction, partial-order reduction, compositional reasoning,
etc. Then,a number of way are proposed for verifying real-time and hybrid systems using model checking. At last,
several approaches combining model checking and other verification techniques or mathematical methods are consid-
ered.展开更多
Software architecture is the highest-level abstraction of a system. It provides a model of the large-scale structural properties of systems. Recently, software architecture has been an important research sub-field of ...Software architecture is the highest-level abstraction of a system. It provides a model of the large-scale structural properties of systems. Recently, software architecture has been an important research sub-field of software engineering. In this paper,our research work focus on refinement methods of software architecture. By studying the several refinement methods for software architectural design,we present a component-based refinement method that refines an architectural design by replacing a component's static semanucs to its dynamic semantics.展开更多
文摘Model checking is an algorithmic verification technique that checks automatically whether a given finite
state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space
explosion problem. In this paper, several important approaches have been proposed for dealing with the state
explosion problem. Such approaches are symbolic, abstraction, partial-order reduction, compositional reasoning,
etc. Then,a number of way are proposed for verifying real-time and hybrid systems using model checking. At last,
several approaches combining model checking and other verification techniques or mathematical methods are consid-
ered.
文摘Software architecture is the highest-level abstraction of a system. It provides a model of the large-scale structural properties of systems. Recently, software architecture has been an important research sub-field of software engineering. In this paper,our research work focus on refinement methods of software architecture. By studying the several refinement methods for software architectural design,we present a component-based refinement method that refines an architectural design by replacing a component's static semanucs to its dynamic semantics.
