A formal approach for the verification of the permission-based security model of Android
DOI:
https://doi.org/10.19153/cleiej.21.2.3Keywords:
Android, Formal idealized model, Reference monitor, Certified implementation, Model-based security testingAbstract
This article reports on our experiences in applying formal methods to verify the security mechanisms of Android. We have developed a comprehensive formal specification of Android's permission model, which has been used to state and prove properties that establish expected behavior of the procedures that enforce the defined access control policy. We are also interested in providing guarantees concerning actual implementations of the mechanisms. Therefore we are following a verification approach that combines the use of idealized models, on which fundamental properties are formally verified, with testing of actual implementations using lightweight model-based techniques. We describe the formalized model, present security properties that have been proved using the Coq proof assistant and propose the use of a certified algorithm for performing verification activities such as monitoring of actual implementations of the platform and also as a testing oracle.
References
[1] Open Handset Alliance, “Android project,” Available at: http://source.android.com/, Last access:
December 2017.
[2] Gartner, “Gartner says worldwide sales of smartphones grew 7 percent in the fourth quarter of 2016,”
Gartner, Inc., Tech. Rep., 2017, available at: http://www.gartner.com/newsroom/id/3609817. Last
access: December 2017.
[3] J. P. Anderson, “Computer Security technology planning study,”
urlhttp://csrc.nist.gov/publications/history/ande72.pdf, Deputy for Command and Management System,
USA, Tech. Rep., 1972. [Online]. Available: http://csrc.nist.gov/publications/history/ande72.pdf
[4] G. Betarte, J. D. Campo, C. Luna, and A. Romano, “Formal analysis of android’s permission-based
security model„” Sci. Ann. Comp. Sci., vol. 26, no. 1, pp. 27–68, 2016. [Online]. Available:
http://dx.doi.org/10.7561/SACS.2016.1.27
[5] Android Developers, “Requesting Permissions at Run Time,” Available at: https://developer.android.
com/intl/es/training/permissions/requesting.html, Last access: December 2017.
[6] The Coq Development Team, The Coq Proof Assistant Reference Manual – Version V8.5, 2016. [Online].
Available: http://coq.inria.fr
[7] P. Letouzey, “A New Extraction for Coq,” in Proceedings of TYPES’02, ser. LNCS, vol. 2646, 2003.
[8] G. Betarte, J. Campo, M. Cristiá, F. Gorostiaga, C. Luna, and C. Sanz, “Towards formal model-based
analysis and testing of android’s security mechanisms,” in Proceedings of CLEI-SLISW ’17, 2017. [Online].
Available: http://www.clei2017-46jaiio.sadio.org.ar/sites/default/files/Mem/SLISW/slisw-02.pdf
[9] Android Open Source Project, “Platform Architecture,” Available at: //developer.android.com/guide/
platform/index.html, Last access: December 2017.
[10] Android Developers, “Application Fundamentals,” Available at: http://developer.android.com/guide/
components/fundamentals.html, Last access: December 2017.
[11] A. P. Felt, E. Chin, S. Hanna, D. Song, and D. Wagner, “Android permissions demystified,” in
Proceedings of CCS ’11, 2011. [Online]. Available: http://doi.acm.org/10.1145/2046707.2046779
[12] A. Armando, G. Costa, and A. Merlo, “Formal modeling and reasoning about the android security
framework,” in TGC 2012, 2012.
[13] Android Developers, “Security Tips,” Available at: http://developer.android.com/training/articles/
security-tips.html, Last access: December 2017.
[14] ——, “<manifest>,” Available at: http://developer.android.com/guide/topics/manifest/
manifest-element.html#uid, Last access: December 2017.
[15] ——, “R.styleable,” Available at: http://developer.android.com/reference/android/R.styleable.html, Last
access: December 2017.
[16] GSI, “Formal verification of the security model of Android: Coq code,” Available at: http://www.
fing.edu.uy/inco/grupos/gsi/documentos/proyectos/Android6-Coq-model.tar.gz, Last access: December
2017.
[17] D. Sbîrlea, M. G. Burke, S. Guarnieri, M. Pistoia, and V. Sarkar, “Automatic detection of
inter-application permission leaks in android applications,” IBM J. Res. Dev., vol. 57, no. 6, pp.
2:10–2:10, Nov. 2013. [Online]. Available: http://dx.doi.org/10.1147/JRD.2013.2284403
[18] E. Chin, A. P. Felt, K. Greenwood, and D. Wagner, “Analyzing inter-application communication in
android,” in Proceedings of MobiSys ’11, 2011.
[19] M. Utting and B. Legeard, Practical Model-Based Testing: A Tools Approach. San Francisco, CA, USA:
Morgan Kaufmann Publishers Inc., 2006.
[20] P. Stocks and D. Carrington, “A Framework for Specification-Based Testing,” IEEE Transactions on
Software Engineering, vol. 22, no. 11, pp. 777–793, Nov. 1996.
[21] J. M. Spivey, The Z Notation: A Reference Manual. Upper Saddle River, NJ, USA: Prentice-Hall, Inc.,
1989.
[22] M. Cristiá, G. Rossi, and C. S. Frydman, “{log} as a test case generator for the Test Template
Framework,” in SEFM, ser. Lecture Notes in Computer Science, R. M. Hierons, M. G. Merayo, and
M. Bravetti, Eds., vol. 8137. Springer, 2013, pp. 229–243.
[23] M. Cristiá, P. Albertengo, C. S. Frydman, B. Plüss, and P. R. Monetti, “Tool support for the test
template framework,” Softw. Test., Verif. Reliab., vol. 24, no. 1, pp. 3–37, 2014. [Online]. Available:
http://dx.doi.org/10.1002/stvr.1477
[24] “OVAL Language,” http://oval.mitre.org/, Last access: December 2017.
[25] “Ovaldi, the OVAL Interpreter reference implementation,” http://oval.mitre.org/language/interpreter.
html, MITRE Corporation, Last access: December 2017.
[26] M. Barrère, G. Betarte, and M. Rodríguez, “Towards Machine-assisted Formal Procedures for the
Collection of Digital Evidence,” in Proceedings of PST’11, 2011.
[27] M. Barrère, H. G., R. Badonnel, and O. Festor, “Increasing Android Security using a Lightweight
OVAL-based Vulnerability Assessment Framework,” in Proceedings of IEEE SafeConfig’12, 2012.
[28] M. Barrare, G. Hurel, R. Badonnel, and O. Festor, “Ovaldroid: An oval-based vulnerability assessment
framework for android,” in 2013 IFIP/IEEE International Symposium on Integrated Network Management
(IM 2013), May 2013, pp. 1074–1075.
[29] Android Developers, “Android NDK,” Available at: https://developer.android.com/guide/topics/security/
permissions.html, Last access: December 2017.
[30] SecurityWeek News, “Bankosy,” Disponible en: http://www.securityweek.com/
android-trojans-exploit-marshmallows-permission-model, Last access: December 2017.
[31] G. Suarez-Tangil, J. E. Tapiador, P. Peris-Lopez, and A. Ribagorda, “Evolution, detection and analysis
of malware for smart devices,” IEEE Communications Surveys and Tutorials, vol. 16, no. 2, pp. 961–987,
2014. [Online]. Available: http://dx.doi.org/10.1109/SURV.2013.101613.00077
[32] M. L. Polla, F. Martinelli, and D. Sgandurra, “A survey on security for mobile devices,” IEEE
Communications Surveys and Tutorials, vol. 15, no. 1, pp. 446–471, 2013. [Online]. Available:
http://dx.doi.org/10.1109/SURV.2012.013012.00028
[33] P. Faruki, A. Bharmal, V. Laxmi, V. Ganmoor, M. S. Gaur, M. Conti, and M. Rajarajan,
“Android security: A survey of issues, malware penetration, and defenses,” IEEE Communications
Surveys and Tutorials, vol. 17, no. 2, pp. 998–1022, 2015. [Online]. Available: http:
//dx.doi.org/10.1109/COMST.2014.2386139
[34] B. Rashidi and C. Fung, “A survey of android security threats and defenses,” Journal of Wireless
Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), vol. 6, no. 3, pp. 3–35,
September 2015.
[35] Sufatrio, D. J. J. Tan, T.-W. Chua, and V. L. L. Thing, “Securing android: A survey, taxonomy,
and challenges,” ACM Comput. Surv., vol. 47, no. 4, pp. 58:1–58:45, May 2015. [Online]. Available:
http://doi.acm.org/10.1145/2733306
[36] M. Conti, V. T. N. Nguyen, and B. Crispo, “Crepe: context-related policy enforcement for android,” in
Proceedings of ISC’10, 2011.
[37] M. Nauman, S. Khan, and X. Zhang, “Apex: extending android permission model and enforcement with
user-defined runtime constraints,” in Proceedings of ASIACCS ’10, 2011.
[38] M. Bugliesi, S. Calzavara, and A. Spanò, “Lintent: Towards security type-checking of android applications,”
in Proceedings of FMOODS/FORTE 2013, 2013.
[39] A. P. Felt, H. J. Wang, A. Moshchuk, S. Hanna, and E. Chin, “Permission re-delegation: Attacks
and defenses.” in USENIX Security Symposium. USENIX Association, 2011. [Online]. Available:
http://dblp.uni-trier.de/db/conf/uss/uss2011.html#FeltWMHC11
[40] A. Armando, R. Carbone, G. Costa, and A. Merlo, “Android permissions unleashed,” in IEEE 28th
Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015, C. Fournet,
M. W. Hicks, and L. Viganò, Eds. IEEE Computer Society, 2015, pp. 320–333. [Online]. Available:
https://doi.org/10.1109/CSF.2015.29
[41] E. Fragkaki, L. Bauer, L. Jia, and D. Swasey, “Modeling and enhancing android’s permission system.” in
Proceedings of ESORICS’12, S. Foresti, M. Yung, and F. Martinelli, Eds., 2012.
[42] W. Shin, S. Kiyomoto, K. Fukushima, and T. Tanaka, “A formal model to analyze the permission
authorization and enforcement in the android framework,” in Proceedings of the 2010 IEEE Second
International Conference on Social Computing. Washington, DC, USA: IEEE Computer Society, 2010,
pp. 944–951. [Online]. Available: http://dx.doi.org/10.1109/SocialCom.2010.140
[43] ——, “A first step towards automated permission-enforcement analysis of the android framework,” in
Proceedings of the 2010 International Conference on Security & Management, SAM 2010, July 12-15,
2010, Las Vegas Nevada, USA, 2 Volumes, H. R. Arabnia, K. Daimi, M. R. Grimaila, G. Markowsky,
S. Aissi, V. A. Clincy, L. Deligiannidis, D. Gabrielyan, G. Margarov, A. M. G. Solo, C. Valli, and P. A. H.
Williams, Eds. CSREA Press, 2010, pp. 323–329.
[44] Z. Paraskevopoulou, C. Hritcu, M. Dénès, L. Lampropoulos, and B. C. Pierce, “Foundational
property-based testing,” in Proceedings of ITP 2015, 2015, pp. 325–343. [Online]. Available:
http://dx.doi.org/10.1007/978-3-319-22102-1_22
[45] C. Dubois, A. Giorgetti, and R. Genestier, “Tests and proofs for enumerative combinatorics,”
in Proceedings of TAP 2016, ser. LNCS, vol. 9762, 2016. [Online]. Available: http:
//dx.doi.org/10.1007/978-3-319-41135-4_4
[46] H. Becker, J. M. Crespo, J. Galowicz, U. Hensel, Y. Hirai, C. Kunz, K. Nakata, J. L. Sacchini, H. Tews,
and T. Tuerk, “Combining mechanized proofs and model-based testing in the formal analysis of a
hypervisor,” in Proceedings of FM 2016, 2016.
[47] T. Tuerk, “Efficiently executable sets used by fireeye,” in The 8th Coq Workshop Nancy, France, August
26, 2016, 2016.
[48] A. D. Brucker and B. Wolff, “On theorem prover-based testing,” Formal Asp. Comput., vol. 25, no. 5,
pp. 683–721, 2013. [Online]. Available: http://dx.doi.org/10.1007/s00165-012-0222-y
[49] Y. Jing, G. Ahn, and H. Hu, “Model-based conformance testing for android,” in Advances
in Information and Computer Security - 7th International Workshop on Security, IWSEC 2012,
Fukuoka, Japan, November 7-9, 2012. Proceedings, ser. Lecture Notes in Computer Science,
G. Hanaoka and T. Yamauchi, Eds., vol. 7631. Springer, 2012, pp. 1–18. [Online]. Available:
https://doi.org/10.1007/978-3-642-34117-5_1
[50] G. de Cleva Farto and A. T. Endo, “Evaluating the model-based testing approach in the context of
mobile applications,” Electr. Notes Theor. Comput. Sci., vol. 314, pp. 3–21, 2015. [Online]. Available:
https://doi.org/10.1016/j.entcs.2015.05.002
[51] M. Cristiá and G. Rossi, “A decision procedure for sets, binary relations and partial functions,” in
Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July
17-23, 2016, Proceedings, Part I, ser. Lecture Notes in Computer Science, vol. 9779, 2016, pp. 179–198.
[Online]. Available: http://dx.doi.org/10.1007/978-3-319-41528-4_10
December 2017.
[2] Gartner, “Gartner says worldwide sales of smartphones grew 7 percent in the fourth quarter of 2016,”
Gartner, Inc., Tech. Rep., 2017, available at: http://www.gartner.com/newsroom/id/3609817. Last
access: December 2017.
[3] J. P. Anderson, “Computer Security technology planning study,”
urlhttp://csrc.nist.gov/publications/history/ande72.pdf, Deputy for Command and Management System,
USA, Tech. Rep., 1972. [Online]. Available: http://csrc.nist.gov/publications/history/ande72.pdf
[4] G. Betarte, J. D. Campo, C. Luna, and A. Romano, “Formal analysis of android’s permission-based
security model„” Sci. Ann. Comp. Sci., vol. 26, no. 1, pp. 27–68, 2016. [Online]. Available:
http://dx.doi.org/10.7561/SACS.2016.1.27
[5] Android Developers, “Requesting Permissions at Run Time,” Available at: https://developer.android.
com/intl/es/training/permissions/requesting.html, Last access: December 2017.
[6] The Coq Development Team, The Coq Proof Assistant Reference Manual – Version V8.5, 2016. [Online].
Available: http://coq.inria.fr
[7] P. Letouzey, “A New Extraction for Coq,” in Proceedings of TYPES’02, ser. LNCS, vol. 2646, 2003.
[8] G. Betarte, J. Campo, M. Cristiá, F. Gorostiaga, C. Luna, and C. Sanz, “Towards formal model-based
analysis and testing of android’s security mechanisms,” in Proceedings of CLEI-SLISW ’17, 2017. [Online].
Available: http://www.clei2017-46jaiio.sadio.org.ar/sites/default/files/Mem/SLISW/slisw-02.pdf
[9] Android Open Source Project, “Platform Architecture,” Available at: //developer.android.com/guide/
platform/index.html, Last access: December 2017.
[10] Android Developers, “Application Fundamentals,” Available at: http://developer.android.com/guide/
components/fundamentals.html, Last access: December 2017.
[11] A. P. Felt, E. Chin, S. Hanna, D. Song, and D. Wagner, “Android permissions demystified,” in
Proceedings of CCS ’11, 2011. [Online]. Available: http://doi.acm.org/10.1145/2046707.2046779
[12] A. Armando, G. Costa, and A. Merlo, “Formal modeling and reasoning about the android security
framework,” in TGC 2012, 2012.
[13] Android Developers, “Security Tips,” Available at: http://developer.android.com/training/articles/
security-tips.html, Last access: December 2017.
[14] ——, “<manifest>,” Available at: http://developer.android.com/guide/topics/manifest/
manifest-element.html#uid, Last access: December 2017.
[15] ——, “R.styleable,” Available at: http://developer.android.com/reference/android/R.styleable.html, Last
access: December 2017.
[16] GSI, “Formal verification of the security model of Android: Coq code,” Available at: http://www.
fing.edu.uy/inco/grupos/gsi/documentos/proyectos/Android6-Coq-model.tar.gz, Last access: December
2017.
[17] D. Sbîrlea, M. G. Burke, S. Guarnieri, M. Pistoia, and V. Sarkar, “Automatic detection of
inter-application permission leaks in android applications,” IBM J. Res. Dev., vol. 57, no. 6, pp.
2:10–2:10, Nov. 2013. [Online]. Available: http://dx.doi.org/10.1147/JRD.2013.2284403
[18] E. Chin, A. P. Felt, K. Greenwood, and D. Wagner, “Analyzing inter-application communication in
android,” in Proceedings of MobiSys ’11, 2011.
[19] M. Utting and B. Legeard, Practical Model-Based Testing: A Tools Approach. San Francisco, CA, USA:
Morgan Kaufmann Publishers Inc., 2006.
[20] P. Stocks and D. Carrington, “A Framework for Specification-Based Testing,” IEEE Transactions on
Software Engineering, vol. 22, no. 11, pp. 777–793, Nov. 1996.
[21] J. M. Spivey, The Z Notation: A Reference Manual. Upper Saddle River, NJ, USA: Prentice-Hall, Inc.,
1989.
[22] M. Cristiá, G. Rossi, and C. S. Frydman, “{log} as a test case generator for the Test Template
Framework,” in SEFM, ser. Lecture Notes in Computer Science, R. M. Hierons, M. G. Merayo, and
M. Bravetti, Eds., vol. 8137. Springer, 2013, pp. 229–243.
[23] M. Cristiá, P. Albertengo, C. S. Frydman, B. Plüss, and P. R. Monetti, “Tool support for the test
template framework,” Softw. Test., Verif. Reliab., vol. 24, no. 1, pp. 3–37, 2014. [Online]. Available:
http://dx.doi.org/10.1002/stvr.1477
[24] “OVAL Language,” http://oval.mitre.org/, Last access: December 2017.
[25] “Ovaldi, the OVAL Interpreter reference implementation,” http://oval.mitre.org/language/interpreter.
html, MITRE Corporation, Last access: December 2017.
[26] M. Barrère, G. Betarte, and M. Rodríguez, “Towards Machine-assisted Formal Procedures for the
Collection of Digital Evidence,” in Proceedings of PST’11, 2011.
[27] M. Barrère, H. G., R. Badonnel, and O. Festor, “Increasing Android Security using a Lightweight
OVAL-based Vulnerability Assessment Framework,” in Proceedings of IEEE SafeConfig’12, 2012.
[28] M. Barrare, G. Hurel, R. Badonnel, and O. Festor, “Ovaldroid: An oval-based vulnerability assessment
framework for android,” in 2013 IFIP/IEEE International Symposium on Integrated Network Management
(IM 2013), May 2013, pp. 1074–1075.
[29] Android Developers, “Android NDK,” Available at: https://developer.android.com/guide/topics/security/
permissions.html, Last access: December 2017.
[30] SecurityWeek News, “Bankosy,” Disponible en: http://www.securityweek.com/
android-trojans-exploit-marshmallows-permission-model, Last access: December 2017.
[31] G. Suarez-Tangil, J. E. Tapiador, P. Peris-Lopez, and A. Ribagorda, “Evolution, detection and analysis
of malware for smart devices,” IEEE Communications Surveys and Tutorials, vol. 16, no. 2, pp. 961–987,
2014. [Online]. Available: http://dx.doi.org/10.1109/SURV.2013.101613.00077
[32] M. L. Polla, F. Martinelli, and D. Sgandurra, “A survey on security for mobile devices,” IEEE
Communications Surveys and Tutorials, vol. 15, no. 1, pp. 446–471, 2013. [Online]. Available:
http://dx.doi.org/10.1109/SURV.2012.013012.00028
[33] P. Faruki, A. Bharmal, V. Laxmi, V. Ganmoor, M. S. Gaur, M. Conti, and M. Rajarajan,
“Android security: A survey of issues, malware penetration, and defenses,” IEEE Communications
Surveys and Tutorials, vol. 17, no. 2, pp. 998–1022, 2015. [Online]. Available: http:
//dx.doi.org/10.1109/COMST.2014.2386139
[34] B. Rashidi and C. Fung, “A survey of android security threats and defenses,” Journal of Wireless
Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), vol. 6, no. 3, pp. 3–35,
September 2015.
[35] Sufatrio, D. J. J. Tan, T.-W. Chua, and V. L. L. Thing, “Securing android: A survey, taxonomy,
and challenges,” ACM Comput. Surv., vol. 47, no. 4, pp. 58:1–58:45, May 2015. [Online]. Available:
http://doi.acm.org/10.1145/2733306
[36] M. Conti, V. T. N. Nguyen, and B. Crispo, “Crepe: context-related policy enforcement for android,” in
Proceedings of ISC’10, 2011.
[37] M. Nauman, S. Khan, and X. Zhang, “Apex: extending android permission model and enforcement with
user-defined runtime constraints,” in Proceedings of ASIACCS ’10, 2011.
[38] M. Bugliesi, S. Calzavara, and A. Spanò, “Lintent: Towards security type-checking of android applications,”
in Proceedings of FMOODS/FORTE 2013, 2013.
[39] A. P. Felt, H. J. Wang, A. Moshchuk, S. Hanna, and E. Chin, “Permission re-delegation: Attacks
and defenses.” in USENIX Security Symposium. USENIX Association, 2011. [Online]. Available:
http://dblp.uni-trier.de/db/conf/uss/uss2011.html#FeltWMHC11
[40] A. Armando, R. Carbone, G. Costa, and A. Merlo, “Android permissions unleashed,” in IEEE 28th
Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015, C. Fournet,
M. W. Hicks, and L. Viganò, Eds. IEEE Computer Society, 2015, pp. 320–333. [Online]. Available:
https://doi.org/10.1109/CSF.2015.29
[41] E. Fragkaki, L. Bauer, L. Jia, and D. Swasey, “Modeling and enhancing android’s permission system.” in
Proceedings of ESORICS’12, S. Foresti, M. Yung, and F. Martinelli, Eds., 2012.
[42] W. Shin, S. Kiyomoto, K. Fukushima, and T. Tanaka, “A formal model to analyze the permission
authorization and enforcement in the android framework,” in Proceedings of the 2010 IEEE Second
International Conference on Social Computing. Washington, DC, USA: IEEE Computer Society, 2010,
pp. 944–951. [Online]. Available: http://dx.doi.org/10.1109/SocialCom.2010.140
[43] ——, “A first step towards automated permission-enforcement analysis of the android framework,” in
Proceedings of the 2010 International Conference on Security & Management, SAM 2010, July 12-15,
2010, Las Vegas Nevada, USA, 2 Volumes, H. R. Arabnia, K. Daimi, M. R. Grimaila, G. Markowsky,
S. Aissi, V. A. Clincy, L. Deligiannidis, D. Gabrielyan, G. Margarov, A. M. G. Solo, C. Valli, and P. A. H.
Williams, Eds. CSREA Press, 2010, pp. 323–329.
[44] Z. Paraskevopoulou, C. Hritcu, M. Dénès, L. Lampropoulos, and B. C. Pierce, “Foundational
property-based testing,” in Proceedings of ITP 2015, 2015, pp. 325–343. [Online]. Available:
http://dx.doi.org/10.1007/978-3-319-22102-1_22
[45] C. Dubois, A. Giorgetti, and R. Genestier, “Tests and proofs for enumerative combinatorics,”
in Proceedings of TAP 2016, ser. LNCS, vol. 9762, 2016. [Online]. Available: http:
//dx.doi.org/10.1007/978-3-319-41135-4_4
[46] H. Becker, J. M. Crespo, J. Galowicz, U. Hensel, Y. Hirai, C. Kunz, K. Nakata, J. L. Sacchini, H. Tews,
and T. Tuerk, “Combining mechanized proofs and model-based testing in the formal analysis of a
hypervisor,” in Proceedings of FM 2016, 2016.
[47] T. Tuerk, “Efficiently executable sets used by fireeye,” in The 8th Coq Workshop Nancy, France, August
26, 2016, 2016.
[48] A. D. Brucker and B. Wolff, “On theorem prover-based testing,” Formal Asp. Comput., vol. 25, no. 5,
pp. 683–721, 2013. [Online]. Available: http://dx.doi.org/10.1007/s00165-012-0222-y
[49] Y. Jing, G. Ahn, and H. Hu, “Model-based conformance testing for android,” in Advances
in Information and Computer Security - 7th International Workshop on Security, IWSEC 2012,
Fukuoka, Japan, November 7-9, 2012. Proceedings, ser. Lecture Notes in Computer Science,
G. Hanaoka and T. Yamauchi, Eds., vol. 7631. Springer, 2012, pp. 1–18. [Online]. Available:
https://doi.org/10.1007/978-3-642-34117-5_1
[50] G. de Cleva Farto and A. T. Endo, “Evaluating the model-based testing approach in the context of
mobile applications,” Electr. Notes Theor. Comput. Sci., vol. 314, pp. 3–21, 2015. [Online]. Available:
https://doi.org/10.1016/j.entcs.2015.05.002
[51] M. Cristiá and G. Rossi, “A decision procedure for sets, binary relations and partial functions,” in
Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July
17-23, 2016, Proceedings, Part I, ser. Lecture Notes in Computer Science, vol. 9779, 2016, pp. 179–198.
[Online]. Available: http://dx.doi.org/10.1007/978-3-319-41528-4_10
Downloads
Published
2018-08-01
Issue
Section
Articles
License
CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).
