Dario Fischbein
Nicolas D’Ippolito
Sebastian Uchitel
Skip Abstract Section
Abstract
Constructing comprehensive operational models of intended system behavior is a complex and costly task, which can be mitigated by the construction of partial behavior models, providing early feedback and subsequently elaborating them iteratively. However, how should partial behavior models with different viewpoints covering different aspects of behavior be composed? How should partial models of component instances of the same type be put together? In this article, we propose model merging of modal transition systems (MTSs) as a solution to these questions. MTS models are a natural extension of labelled transition systems that support explicit modeling of what is currently unknown about system behavior. We formally define model merging based on weak alphabet refinement, which guarantees property preservation, and show that merging consistent models is a process that should result in a minimal common weak alphabet refinement (MCR). In this article, we provide theoretical results and algorithms that support such a process. Finally, because in practice MTS merging is likely to be combined with other operations over MTSs such as parallel composition, we also study the algebraic properties of merging and apply these, together with the algorithms that support MTS merging, in a case study.
- Abadi, M. and Lamport, L. 1991. The existence of refinement mappings. Theor. Comput. Sci. 82, 2, 253--284. Google Scholar
Digital Library
- Ball, T., Levin, V., and Xie, F. 2004. Automatic creation of environment models via training. In Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04). Lecture Notes in Computer Science, vol. 2988, Springer, Berlin, 93--107.Google Scholar
- Boem, B. and Turner, R. 2004. Balancing agility and discipline: A Guide for the Perplexed. Pearson Education. Google ScholarDigital Library
- Brunet, G. 2006. A characterization of merging partial behavioral models. M.S. thesis, University of Toronto.Google Scholar
- Bruns, G. and Godefroid, P. 1999. Model checking partial state spaces with 3-valued temporal logics. In Proceedings of 11th International Conference on Computer-Aided Verification (CAV’99). Lecture Notes in Computer Science, vol. 1633, Springer, Berlin, 274--287. Google ScholarDigital Library
- Bruns, G. and Godefroid, P. 2000. Generalized model checking: Reasoning about partial state spaces. In Proceedings of 11th International Conference on Concurrency Theory (CONCUR’00). Lecture Notes in Computer Science, vol. 1877, Springer, 168--182. Google ScholarDigital Library
- Calder, M. and Magill, E. H., (eds.). 2000. Feature Interactions in Telecommunications and Software Systems VI. IOS Press. Google ScholarDigital Library
- Chechik, M., Devereux, B., Easterbrook, S., and Gurfinkel, A. 2003. Multi-valued symbolic model-checking. ACM Trans. Soft. Eng. Methodol. 12, 4, 1--38. Google ScholarDigital Library
- Clarke, E. and Wing, J. 1996. Formal methods: State of the art and future directions. ACM Comput. Surv. 28, 4, 626--643. Google ScholarDigital Library
- Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2001. Progress on the state explosion problem in model checking. In Informatics. 10 Years Back. 10 Years Ahead, R. Wilhelm, Ed., Lecture Notes in Computer Science, vol. 2000, Springer, Berlin, 176--194. Google ScholarDigital Library
- Crews. 1999. Cooperative requirements engineering with scenarios. http://Sunsite.Informatik.RWTH-Aachen.DE/CREWS. Google ScholarDigital Library
- Cunningham, J. and Finkelstein, A. 1986. Formal requirements specification: The FOREST project. In Proceedings of 3rd International Workshop on Software Specification and Design. IEEE Computer Society Press, 186--192.Google Scholar
- Dams, D. 1996. Abstract interpretation and partition refinement for model checking. Ph.D. dissertation, Eindhoven University of Technology, The Netherlands.Google Scholar
- Dams, D., Gerth, R., and Grumberg, O. 1997. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Sys. 2, 19, 253--291. Google ScholarDigital Library
- Diaz-Redondo, R., Pazos-Arias, J., and Fernandez-Vilas, A. 2002. Reusing verification information of incomplete specifications. In Proceedings of the 5th Workshop on Component-Based Software Engineering.Google Scholar
- D’Ippolito, N., Fishbein, D., Chechik, M., and Uchitel, S. 2008. MTSA: The modal transition system analyzer. In Proceedings of International Conference on Automated Software Engineering (ASE’08). 475--476. Google ScholarDigital Library
- Dupont, P., Lambeau, B., Damas, C., and van Lamsweerde, A. 2008. The QSM algorithm and its application to software behavior model induction. J. Appl. Artif. Intell. 22, 1--2, 77--115. Google ScholarDigital Library
- Dwyer, M. B., Avrunin, G. S., and Corbett, J. C. 1998. Property specification patterns for finite-state verification. In Proceedings of 2nd Workshop on Formal Methods in Software Practice. Google ScholarDigital Library
- Easterbrook, S. and Chechik, M. 2001. A framework for multi-valued reasoning over inconsistent viewpoints. In Proceedings of International Conference on Software Engineering (ICSE’01). IEEE Los Alamitos, CA. 411--420. Google ScholarDigital Library
- Fischbein, D. and Uchitel, S. 2008. On correct and complete merging of partial behavior models. In Proceedings of SIGSOFT Conference on Foundations of Software Engineering (FSE’08). 297--307. Google ScholarDigital Library
- Fischbein, D., Uchitel, S., and Braberman, V. A. 2006. A foundation for behavioral conformance in software product line architectures. In Proceedings of ISSTA’06 Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA’06). 39--48. Google ScholarDigital Library
- Fitting, M. 1991. Many-valued modal logics. Fundamenta Inf. 15, 3--4, 335--350. Google ScholarDigital Library
- Giannakopoulou, D. and Magee, J. 2003. Fluent model checking for event-based systems. In Proceedings of the 9th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE’03). ACM, New York, 257--266. Google ScholarDigital Library
- Godefroid, P., Huth, M., and Jagadeesan, R. 2001. Abstraction-based model checking using modal transition systems. In Proceedings of 12th International Conference on Concurrency Theory (CONCUR’01), K. Larsen and M. Nielsen, Eds., Lecture Notes in Computer Science, vol. 2154, Springer, Berlin, 426--440. Google ScholarDigital Library
- Godefroid, P. and Jagadeesan, R. 2003. On the expressiveness of 3-valued models. In Proceedings of 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’03). Lecture Notes in Computer Science, vol. 2575, Springer, Berlin, 206--222. Google ScholarDigital Library
- Godefroid, P. and Pitterman, N. 2009. LTL generalized model checking revisited. In Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’09). Lecture Notes in Computer Science, vol. 5403, Springer, Berlin, 89--104. Google ScholarDigital Library
- Gunter, C. 1992. The mixed powerdomain. Theor. Comput. Sci. 103, 2, 311--334. Google ScholarDigital Library
- Gurfinkel, A. and Chechik, M. 2005. How thorough is thorough enough. In Proceedings of 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’05). Lecture Notes in Computer Science, vol. 3725, Springer, Berlin, 65--80. Google ScholarDigital Library
- Gurfinkel, A., Wei, O., and Chechik, M. 2006. Systematic construction of abstractions for model-checking. In Proceedings of 7th International Conference on Verification, Model-Checking, and Abstract Interpretation (VMCAI’06). Lecture Notes in Computer Science, vol. 3855. Springer, Berlin, 381--397. Google ScholarDigital Library
- Harel, D., Kugler, H., and Pnueli, A. 2005. Synthesis revisited: Generating statechart models from scenario-based requirements. In Formal Methods in Software and Systems Modeling, 309--324.Google Scholar
- Hennessy, M. and Milner, R. 1985. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM 32, 1, 137--161. Google ScholarDigital Library
- Hoare, C. 1985. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Horwitz, S., Prins, J., and Reps, T. 1989. Integrating noninterfering versions of programs. ACM Trans. Program. Lang. Syst. 11, 3, 345--387. Google ScholarDigital Library
- Hunter, A. and Nuseibeh, B. 1998. Managing inconsistent specifications: Reasoning, analysis and action. ACM Trans. Softw. Eng. Methodol. 7, 4, 335--367. Google ScholarDigital Library
- Hussain, A. and Huth, M. 2004. On model checking multiple hybrid views. In Proceedings of 1st International Symposium on Leveraging Applications of Formal Methods. 235--242.Google Scholar
- Huth, M., Jagadeesan, R., and Schmidt, D. A. 2001. Modal transition systems: A foundation for three-valued program analysis. In Proceedings of 10th European Symposium on Programming (ESOP’01). Lecture Notes in Computer Science, vol. 2028. Springer, Berlin, 155--169. Google ScholarDigital Library
- Huth, M., Jagadeesan, R., and Schmidt, D. 2002. A domain equation for refinement of partial systems. Math. Structures Comput. Sci. 14, 4. Google ScholarDigital Library
- Hüttel, H. and Larsen, K. G. 1989. The use of static constructs in a modal process logic. In Proceedings of Symposium on Logical Foundations of Computer Science (Logic at Botik’89). Lecture Notes in Computer Science, vol. 363. 163--180. Google ScholarDigital Library
- IEEE. 1994. IEEE recommended practice for software requirements specifications standard 830. Tech. Standard 830.Google Scholar
- ITU-T. 1993. ITU-T recommendation Z.120: message sequence chart (MSC).Google Scholar
- Jacobson, I. 2004. Object-Oriented Software Engineering: A Use Case Driven Approach. Addison Wesley, Redwood City, CA. Google ScholarDigital Library
- Kazhamiakin, R., Pistore, M., and Roveri, M. 2004. Formal verification of requirements using SPIN: A case study on web services. In Proceedings of International Conference on Software Engineering and Formal Methods (SEFM’04). 406--415. Google ScholarDigital Library
- Kleene, S. C. 1952. Introduction to Metamathematics. Van Nostrand, New York.Google Scholar
- Keller, R. 1976. Formal verification of parallel programs. Comm. ACM 19, 7, 371--384. Google ScholarDigital Library
- Kramer, J., Magee, J., and Sloman, M. 1983. CONIC: An integrated approach to distributed computer control systems. IEE Proc. 130, 1, 1--10.Google ScholarCross Ref
- Krueger, I., Grosu, R., Scholz, P., and Broy, M. 1999. From MSCs to statecharts. In Distributed and Parallel Embedded Systems, F. J. Rammig, Ed. Kluwer, Amsterdam. Google ScholarDigital Library
- Larsen, K. and Thomsen, B. 1988. A modal process logic. In Proceedings of 3rd Annual Symposium on Logic in Computer Science (LICS’88). IEEE, Los Alamitos, CA. 203--210.Google Scholar
- Larsen, K. and Xinxin, L. 1990. Equation solving using modal transition systems. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS’90). IEEE, Los Alamitos, CA, 108--117.Google Scholar
- Larsen, K. G., Steffen, B., and Weise, C. 1995. A constraint oriented proof methodology based on modal transition systems. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS’95). Lecture Notes in Computer Science, vol. 1019, Springer, Berlin, 13--28. Google ScholarDigital Library
- Larsen, K., Steffen, B., and Weise, C. 1996. The methodology of modal constraints. In Formal Systems Specification. Lecture Notes in Computer Science, vol. 1169, Springer, Berlin, 405--435. Google ScholarDigital Library
- Letier, E., Kramer, J., Magee, J., and Uchitel, S. 2008. Deriving event-based transition systems from goal-oriented requirements models. Autom. Softw. Eng. 15, 2, 175--206. Google ScholarDigital Library
- Magee, J. and Kramer, J. 1999. Concurrency - State Models and Java Programs. Wiley, New York. Google ScholarDigital Library
- Milner, R. 1989. Communication and Concurrency. Prentice-Hall, New York. Google ScholarDigital Library
- Nejati, S. and Chechik, M. 2005. Let’s agree to disagree. In Proceedings of 20th IEEE International Conference on Automated Software Engineering (ASE’05). IEEE, Los Alamitos, CA. 287--290. Google ScholarDigital Library
- Nejati, S. and Chechik, M. 2008. Behavioral model fusion: Experiences from two telecommunication case studies. In Proceedings of ICSE’08 Workshop on Modeling in Software Engineering (MiSE’08). Google ScholarDigital Library
- Nejati, S., Sabetzadeh, M., Chechik, M., Easterbrook, S., and Zave, P. 2007. Matching and merging of statecharts specifications. In Proceedings of the 29th International Conference on Software Engineering (ICSE’07). 54--64. Google ScholarDigital Library
- Nejati, S., Chechik, M., Sabetzadeh, M., Uchitel, S., and Zave, P. 2008. Towards compositional synthesis of evolving systems. In Proceedings of the SIGSOFT Conference on Foundations of Software Engineering (FSE’08). 285--296. Google ScholarDigital Library
- Pnueli, A. 1977. The temporal logic of programs. In Proceedings of 18th Annual Symposium on the Foundations of Computer Science. 46--57. Google ScholarDigital Library
- Sabetzadeh, M. and Easterbrook, S. 2003. Analysis of inconsistency in graph-based viewpoints: A category-theoretic approach. In Proceedings of 18th IEEE International Conference on Automated Software Engineering (ASE’03). IEEE, Los Alamitos, CA. 12--21.Google Scholar
- Shoham, S. and Grumberg, O. 2004. Monotonic abstraction-refinement for CTL. In Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04). Lecture Notes in Computer Science, vol. 2988, Springer, Berlin, 546--560.Google Scholar
- Sibay, G., Uchitel, S., and Braberman, V. 2008. Existential live sequence charts revisited. In Proceedings of the 30th International Conference on Software Engineering (ICSE’08). ACM, New York, 41--50. Google ScholarDigital Library
- Uchitel, S. and Chechik, M. 2004. Merging partial behavioral models. In Proceedings of 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM, New York, 43--52. Google ScholarDigital Library
- Uchitel, S., Kramer, J., and Magee, J. 2003a. Behavior model elaboration using partial labelled transition systems. In Proceedings of the 9th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE’03). ACM, New York, 19--27. Google ScholarDigital Library
- Uchitel, S., Kramer, J., and Magee, J. 2003b. Synthesis of behavioral models from scenarios. IEEE Trans. Soft. Eng. 29, 2, 99--115. Google ScholarDigital Library
- Uchitel, S., Kramer, J., and Magee, J. 2004. Incremental elaboration of scenario-based specifications and behavior models using implied scenarios. ACM Trans. Soft. Eng. Methodol. 13, 1, 37--85. Google ScholarDigital Library
- Uchitel, S., Broy, M., Krueger, I. H., and Whittle, J. 2005. Guest editorial: Special section on interaction and state-based modeling. IEEE Trans. Softw. Eng. 31, 12, 997--998. Google ScholarDigital Library
- Uchitel, S., Brunet, G., and Chechik, M. 2007. Behavior model synthesis from properties and scenarios. In Proceedings of International Conference on Software Engineering (ICSE’07). 34--43. Google ScholarDigital Library
- Uchitel, S., Brunet, G., and Chechik, M. 2009. Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Soft. Eng. 3, 35, 384--406. Google ScholarDigital Library
- van Lamsweerde, A. 2004. Goal-oriented requirements enginering: A roundtrip from research to practice. In Proceedings of the 12th IEEE International Conference on Requirements Engineering. IEEE, Los Alamitos, CA. 4--7. Google ScholarDigital Library
- van Lamsweerde, A. and Letier, E. 2000. Handling obstacles in goal-oriented requirements engineering. IEEE Trans. Soft. Eng. 26, 10, 978--1005. Google ScholarDigital Library
- van Ommering, R., van der Linden, F., Kramer, J., and Magee, J. 2000. The Koala component model for consumer electronics software. IEEE Computer 33, 3, 78--85. Google ScholarDigital Library
- Wei, O., Gurfinkel, A., and Chechik, M. 2009. Mixed transition systems revisited. In Proceedings of 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’09). Lecture Notes in Computer Science, vol. 5403, 349--365. Google ScholarDigital Library
- Xing, Z. and Stroulia, E. 2005. UMLDiff: An algorithm for object-oriented design differencing. In Proceedings of 20th IEEE International Conference on Automated Software Engineering (ASE’05). IEEE, Los Alamitos, CA. 54--65. Google ScholarDigital Library
Index Terms
- Weak Alphabet Merging of Partial Behavior Models
Recommendations
On correct and complete strong merging of partial behaviour models
SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineeringModal Transition Systems (MTS) have been shown to be useful to reason about system behaviour in the context of partial information and to support incremental elaboration of behaviour models. A particularly useful notion in the context of software and ...
Merging partial behavioural models
Constructing comprehensive operational models of intended system behaviour is a complex and costly task. Consequently, practitioners have adopted techniques that support incremental elaboration of partial behaviour descriptions. A noteworthy example is ...
Synthesizing Modal Transition Systems from Triggered Scenarios
Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which ...
Comments