Automated environment generation for software model checking Export

@inproceedings{citeulike:4012233, abstract = {A key problem in model checking open systems is environment modeling (i.e., representing the behavior of the execution context of the system under analysis). Software systems are fundamentally open since their behavior is dependent on patterns of invocation of system components and values defined outside the system but referenced within the system. Whether reasoning about the behavior of whole programs or about program components, an abstract model of the environment can be essential in enabling sufficiently precise yet tractable verification. In this paper, we describe an approach to generating environments of Java program fragments. This approach integrates formally specified assumptions about environment behavior with sound abstractions of environment implementations to form a model of the environment. The approach is implemented in the Bandera Environment Generator (BEG) which we describe along with our experience using BEG to reason about properties of several non-trivial concurrent Java programs. 1}, author = {Tkachuk, Oksana and Dwyer, Matthew B.}, booktitle = {In Proceedings of the 18th International Conference on Automated Software Engineering}, citeulike-article-id = {4012233}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.1681}, keywords = {2003, bandera, modelchecking, tool}, pages = {116--129}, posted-at = {2009-02-05 14:22:41}, priority = {2}, title = {Automated environment generation for software model checking}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.1681}, year = {2003} }

TY - CONF ID - citeulike:4012233 L3 - citeulike-article-id:4012233 N2 - A key problem in model checking open systems is environment modeling (i.e., representing the behavior of the execution context of the system under analysis). Software systems are fundamentally open since their behavior is dependent on patterns of invocation of system components and values defined outside the system but referenced within the system. Whether reasoning about the behavior of whole programs or about program components, an abstract model of the environment can be essential in enabling sufficiently precise yet tractable verification. In this paper, we describe an approach to generating environments of Java program fragments. This approach integrates formally specified assumptions about environment behavior with sound abstractions of environment implementations to form a model of the environment. The approach is implemented in the Bandera Environment Generator (BEG) which we describe along with our experience using BEG to reason about properties of several non-trivial concurrent Java programs. 1 EP - 129 TI - Automated environment generation for software model checking T2 - In Proceedings of the 18th International Conference on Automated Software Engineering SP - 116 KW - 2003 KW - bandera KW - modelchecking KW - tool AU - Tkachuk, Oksana AU - Dwyer, Matthew PY - 2003/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.1681 ER -