Integration of model checking into software development processes Export

@phdthesis{citeulike:271388, abstract = {Testing has been the dominant method for validation of software systems. As software systems become complex, conventional testing methods have become inadequate. Model checking is a powerful formal verification method. It supports systematic exploration of all states or execution paths of the system being verified. There are two major challenges in practical and scalable application of model checking to software systems: (1)\&nbsp;the applicability of model checking to software systems and (2)\&nbsp;the intrinsic complexity of model checking. In this dissertation, we have developed a comprehensive approach to integration of model checking into two emerging software development processes: Model-Driven Development (MDD) and Component-Based Development (CBD), and a combination of MDD and CBD. This approach addresses the two major challenges under the following framework: (1)\&nbsp;bridging applicability gaps through automatic translation of software representations to directly model-checkable formal representations, (2)\&nbsp;seamless integration of state space reduction algorithms in the translation through static analysis, and (3)\&nbsp;scaling model checking capability and achieving state space reduction by systematically exploring compositional structures of software systems. We have integrated model checking into MDD by applying mature model checking techniques to industrial design-level software representations through <italic>automatic translation</italic> of these representations to the input formal representations of model checkers. We have developed a <italic>translation-based</italic> approach to compositional reasoning of software systems, which simplifies the proof, implementation, and application of compositional reasoning rules at the software system level by reusing the proof and implementation of existing compositional reasoning rules for directly model-checkable formal representations. We have developed an integrated state space reduction framework which systematically conducts a <italic>top-down</italic> decomposition of a large and complex software system into directly model-checkable components by exploring domain-specific knowledge. We have designed, implemented, and applied a <italic>bottom-up </italic> approach to model checking of component-based software systems, which composes verified systems from verified components and integrates model checking into CBD. We have further scaled model checking of component-based systems by exploring the synergy between MDD and CBD, i.e., specifying components in executable design languages, and realizing the bottom-up approach based on model checking of software designs through translation.}, author = {Xie, Fei}, citeulike-article-id = {271388}, citeulike-linkout-0 = {http://wwwlib.umi.com/dissertations/fullcit/3143493}, keywords = {cbd, component-based, development, mda, mdd, mdsd, model-checking, model-driven, models, software}, posted-at = {2008-10-24 07:22:42}, priority = {2}, school = {THE UNIVERSITY OF TEXAS AT AUSTIN}, title = {Integration of model checking into software development processes}, url = {http://wwwlib.umi.com/dissertations/fullcit/3143493}, year = {2004} }

TY - THES ID - citeulike:271388 L3 - citeulike-article-id:271388 N2 - Testing has been the dominant method for validation of software systems. As software systems become complex, conventional testing methods have become inadequate. Model checking is a powerful formal verification method. It supports systematic exploration of all states or execution paths of the system being verified. There are two major challenges in practical and scalable application of model checking to software systems: (1)&nbsp;the applicability of model checking to software systems and (2)&nbsp;the intrinsic complexity of model checking. In this dissertation, we have developed a comprehensive approach to integration of model checking into two emerging software development processes: Model-Driven Development (MDD) and Component-Based Development (CBD), and a combination of MDD and CBD. This approach addresses the two major challenges under the following framework: (1)&nbsp;bridging applicability gaps through automatic translation of software representations to directly model-checkable formal representations, (2)&nbsp;seamless integration of state space reduction algorithms in the translation through static analysis, and (3)&nbsp;scaling model checking capability and achieving state space reduction by systematically exploring compositional structures of software systems. We have integrated model checking into MDD by applying mature model checking techniques to industrial design-level software representations through <italic>automatic translation</italic> of these representations to the input formal representations of model checkers. We have developed a <italic>translation-based</italic> approach to compositional reasoning of software systems, which simplifies the proof, implementation, and application of compositional reasoning rules at the software system level by reusing the proof and implementation of existing compositional reasoning rules for directly model-checkable formal representations. We have developed an integrated state space reduction framework which systematically conducts a <italic>top-down</italic> decomposition of a large and complex software system into directly model-checkable components by exploring domain-specific knowledge. We have designed, implemented, and applied a <italic>bottom-up </italic> approach to model checking of component-based software systems, which composes verified systems from verified components and integrates model checking into CBD. We have further scaled model checking of component-based systems by exploring the synergy between MDD and CBD, i.e., specifying components in executable design languages, and realizing the bottom-up approach based on model checking of software designs through translation. TI - Integration of model checking into software development processes PB - THE UNIVERSITY OF TEXAS AT AUSTIN KW - cbd KW - component-based KW - development KW - mda KW - mdd KW - mdsd KW - model-checking KW - model-driven KW - models KW - software AU - Xie, Fei PY - 2004/// UR - http://wwwlib.umi.com/dissertations/fullcit/3143493 ER -