%0 Generic %1 Duarte2008 %A Duarte, L. M. %A Kramer, J. %A Uchitel, S. %B Proceedings of FASE 2008 %C Budapest, Hungary %D 2008 %I Springer %J Lecture Notes in Computer Science %K %P 101-115 %R http://dx.doi.org/10.1007/978-3-540-78743-3 %T Towards Faithful Model Extraction Based on Contexts %U http://www.springerlink.com/content/3710527765155187/ %V 4961 %X Behaviour models facilitate the analysis of software systems using model-checking tools to detect errors and generate counter-examples. Such models can be generated from existing implementations using a model extraction process. This process should guarantee that an extracted model is a faithful representation of the system, so that analysis results may be trusted. This paper discusses the formal foundations of our model extraction process based on contexts. Contexts are abstractions of concrete states of a system, providing valuable information about dependencies between actions. Models are generated by a tool called LTS Extractor and can be re¯ned to improve correctness by augmenting context information. This refinement process eliminates some false negatives and is property-preserving. Completeness of the models depends on the coverage provided by a set of traces describing behaviours of the system. We discuss the faithfulness of our models and results of two case studies.

@conference{Duarte2008, abstract = {Behaviour models facilitate the analysis of software systems using model-checking tools to detect errors and generate counter-examples. Such models can be generated from existing implementations using a model extraction process. This process should guarantee that an extracted model is a faithful representation of the system, so that analysis results may be trusted. This paper discusses the formal foundations of our model extraction process based on contexts. Contexts are abstractions of concrete states of a system, providing valuable information about dependencies between actions. Models are generated by a tool called LTS Extractor and can be re¯ned to improve correctness by augmenting context information. This refinement process eliminates some false negatives and is property-preserving. Completeness of the models depends on the coverage provided by a set of traces describing behaviours of the system. We discuss the faithfulness of our models and results of two case studies.}, added-at = {2012-08-06T21:20:20.000+0200}, address = {Budapest, Hungary}, author = {Duarte, L. M. and Kramer, J. and Uchitel, S.}, biburl = {https://www.bibsonomy.org/bibtex/2bcf6998a0684152abc1109ad9c88ec97/lucio_duarte}, booktitle = {Proceedings of FASE 2008}, doi = {http://dx.doi.org/10.1007/978-3-540-78743-3}, file = {:D\:\\documentos\\documentos\\Conferences\\FASE2008\\Paper\\fase08.pdf:PDF}, groups = {public}, interhash = {66e1a6bf52777d993601ab26fcb7638a}, intrahash = {bcf6998a0684152abc1109ad9c88ec97}, journal = {Lecture Notes in Computer Science}, keywords = {}, month = {April}, pages = {101-115}, publisher = {Springer}, series = {LNCS}, timestamp = {2012-08-06T21:20:20.000+0200}, title = {Towards Faithful Model Extraction Based on Contexts}, url = {http://www.springerlink.com/content/3710527765155187/}, username = {lucio_duarte}, volume = 4961, year = 2008 }