Specification Patterns: Formal and Easy
Property specification is still one of the most challenging tasks for transference of software verification technology. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satisfied. When validatin...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
World Scientific Publishing Co. Pte Ltd
2015
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 09738caa a22009977a 4500 | ||
|---|---|---|---|
| 001 | PAPER-13833 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518204415.0 | ||
| 008 | 190411s2015 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-84941918609 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 030 | |a ISEKE | ||
| 100 | 1 | |a Asteasuain, F. | |
| 245 | 1 | 0 | |a Specification Patterns: Formal and Easy |
| 260 | |b World Scientific Publishing Co. Pte Ltd |c 2015 | ||
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Alfonso, A., Braberman, V., Kicillof, N., Olivero, A., Visual timed event scenarios (2004) 6th ICSE'04, pp. 168-177 | ||
| 504 | |a Asteasuain, F., Braberman, V., Specification patterns can be formal and also easy (2010) Software Engineering and Knowledge Engineering (SEKE), pp. 430-436 | ||
| 504 | |a Autili, M., Inverardi, P., Pelliccione, P., Graphical scenarios for specifying temporal properties: An automated approach (2007) ASE, 14 (3), pp. 293-340 | ||
| 504 | |a Autili, M., Pelliccione, P., Towards a graphical tool for refining user to system requirements (2008) ENTCS, 211, pp. 147-157 | ||
| 504 | |a Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A., Speeding up model checking of timed-models by combining scenario specialization and live component analysis (2009) FORMATS, , Springer | ||
| 504 | |a Braberman, V., Kicillof, N., Olivero, A., A scenario-matching approach to the description and model checking of real-time properties (2005) IEEE TSE, 31 (12), pp. 1028-1041 | ||
| 504 | |a Clarke, E., Grumberg, O., Peled, D., (1999) Model Checking, , MIT Press | ||
| 504 | |a Cobleigh, R., Avrunin, G., Clarke, L., User guidance for creating precise and accessible property specifications (2006) Proc. of 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ACM, p. 218 | ||
| 504 | |a Dalal, S., Jain, A., Karunanithi, N., Leaton, J., Lott, C., Patton, G., Horowitz, B., Modelbased testing in practice (1999) ICSE, pp. 285-294 | ||
| 504 | |a Dillon, L., Kutty, G., Moser, L., Melliar-Smith, P., Ramakrishna, Y., A graphical interval logic for specifying concurrent systems (1994) ACM Trans. Software Engineering and Methodology, 3 (2), pp. 131-165 | ||
| 504 | |a D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., Synthesis of live behaviour models (2010) Proc. of 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering | ||
| 504 | |a Dwyer, M., Avrunin, G., Corbett, J., Specification Patterns Web Site, , http://patterns.projects.cis.ksu.edu/documentation/patterns.shtml | ||
| 504 | |a Dwyer, M., Avrunin, G., Corbett, J., Patterns in property specifications for finitestate verification (1999) Proc. of 21st International Conference on Software Engineering (ICSE), 99 | ||
| 504 | |a Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) Proc. of 9th European Software Engineering Conference, p. 266 | ||
| 504 | |a Grohe, M., Schweikardt, N., The succinctness of first-order logic on linear orders (2004) Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 438-447 | ||
| 504 | |a Harel, D., Marelly, R., Playing with time: On the specification and execution of timeenriched LSCS MASCOTS '02, pp. 193-202 | ||
| 504 | |a Holzmann, G., The logic of bugs (2002) ACM Software Engineering Notes, 27 (6), pp. 81-87 | ||
| 504 | |a Konrad, S., Cheng, B., Real-time specification patterns (2005) Proc. of 27th ICSE, pp. 372-381 | ||
| 504 | |a Laroussinie, F., Markey, N., Schnoebelen, P., Temporal logic with forgettable past (2002) Proceedings of Symposium on Logic in Computer Science, pp. 383-392 | ||
| 504 | |a Leavens, G., Baker, A., Ruby, C., Preliminary design of JML: A behavioral interface specification language for Java (2006) ACM SIGSOFT Software Engineering Notes, 31 (3), pp. 1-38 | ||
| 504 | |a Manna, Z., Pnueli, A., A hierarchy of temporal properties (1987) Proc. of Ninth ACM PODC, pp. 205-205 | ||
| 504 | |a Manna, Z., Pnueli, A., Completing the temporal picture (1989) Automata, Languages and Programming, pp. 534-558 | ||
| 504 | |a Manna, Z., Pnueli, A., (1995) A Temporal Proof Methodology for Reactive Systems, , Springer-Verlag | ||
| 504 | |a Markey, N., Temporal logic with past is exponentially more succinct (2003) EATCS Bull., 79, pp. 122-128 | ||
| 504 | |a Parnas, D., On the criteria to be used in decomposing systems into modules (1972) Commun. ACM, 15 (12), pp. 1053-1058 | ||
| 504 | |a Paun, D., Chechik, M., Events in linear-time properties (1999) Proc. of 4th International Conference on Requirements Engineering | ||
| 504 | |a Piterman, N., Pnueli, A., Sa'ar, Y., Synthesis of reactive (1) designs (2006) Lecture Notes in Computer Science, 3855, pp. 364-380 | ||
| 504 | |a Pradella, M., San Pietro, P., Spoletini, P., Morzenti, A., Practical model checking of LTL with past (2003) ATVA03 | ||
| 504 | |a Viggers, K., Implementing protocols via declarative event patterns (2004) ACM Sigsoft International Symposium on FSE, pp. 158-169 | ||
| 504 | |a Sengupta, B., Cleaveland, R., Triggered message sequence charts (2002) SIGSOFT FSE, pp. 167-176 | ||
| 504 | |a Smith, M., Holzmann, G., Etessami, K., Events and constraints: A graphical editor for capturing logic requirements of programs (2001) Proc. of 5th IEEE RE, pp. 14-22 | ||
| 504 | |a Smith, R., Avrunin, G., Clarke, L., Osterweil, L., Propel: An approach supporting property elucidation (2002) ICSE, 24, pp. 11-21 | ||
| 504 | |a Uchitel, S., Kramer, J., Magee, J., Negative scenarios for implied scenario elicitation (2002) Proc. of FSE, pp. 109-118 | ||
| 504 | |a Utting, M., Legeard, B., (2007) Practical Model-based Testing: A Tools Approach, , Morgan Kaufmann | ||
| 504 | |a Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L., Model-based testing of object-oriented reactive systems with spec explorer (2008) Formal Methods and Testing, pp. 39-76 | ||
| 504 | |a Wilke, T., CTL+ is exponentially more succinct than CTL (1999) Foundations of Software Technology and Theoretical Computer Science, pp. 110-121 | ||
| 520 | 3 | |a Property specification is still one of the most challenging tasks for transference of software verification technology. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satisfied. When validating the desired property the developer may have to deal with the pattern representation in some particular formalism. For this reason, we identify four desirable quality attributes for the underlying specification language: succinctness, comparability, complementariness, and modifiability. We show that typical formalisms such as temporal logics or automata fail at some extent to support these features. Given this context we introduce Featherweight Visual Scenarios (FVS), a declarative and graphical language based on scenarios, as a possible alternative to specify behavioral properties. We illustrate FVS applicability by modeling all the specification patterns and we thoroughly compare FVS to other known approaches, showing that FVS specifications are better suited for validation tasks. In addition, we augment pattern specification by introducing the concept of violating behavior. Finally we characterize the type of properties that can be written in FVS and we formally introduce its syntax and semantics. © 2015 World Scientific Publishing Company. |l eng | |
| 536 | |a Detalles de la financiación: Agencia Nacional de Promoción Científica y Tecnológica, PICT 1774/11, UBACYT W0813, MEALS 295261, UBACYT 20020130100384BA, 0724/12 | ||
| 536 | |a Detalles de la financiación: *This work was partially funded by ANPCYT PICT 1774/11 and 0724/12, UBACYT W0813, UBACYT 20020130100384BA and MEALS 295261. Víctor Braberman is also a±liated to CONICET. | ||
| 593 | |a Dpto. Computación, FCEyN, UBA, Pabellón i, Ciudad Universitaria, (C1428EGA), Buenos Aires, Argentina | ||
| 593 | |a CONICET, Argentina | ||
| 690 | 1 | 0 | |a BEHAVIORAL MODELING |
| 690 | 1 | 0 | |a REQUIREMENTS ENGINEERING |
| 690 | 1 | 0 | |a SPECIFICATION PATTERNS |
| 690 | 1 | 0 | |a COMPUTATIONAL LINGUISTICS |
| 690 | 1 | 0 | |a COMPUTER HARDWARE DESCRIPTION LANGUAGES |
| 690 | 1 | 0 | |a FORMAL LANGUAGES |
| 690 | 1 | 0 | |a REQUIREMENTS ENGINEERING |
| 690 | 1 | 0 | |a SEMANTICS |
| 690 | 1 | 0 | |a SPECIFICATION LANGUAGES |
| 690 | 1 | 0 | |a VERIFICATION |
| 690 | 1 | 0 | |a VISUAL LANGUAGES |
| 690 | 1 | 0 | |a BEHAVIORAL MODEL |
| 690 | 1 | 0 | |a BEHAVIORAL PROPERTIES |
| 690 | 1 | 0 | |a GRAPHICAL LANGUAGES |
| 690 | 1 | 0 | |a PATTERN REPRESENTATION |
| 690 | 1 | 0 | |a PATTERN SPECIFICATIONS |
| 690 | 1 | 0 | |a PROPERTY SPECIFICATION |
| 690 | 1 | 0 | |a SOFTWARE VERIFICATION |
| 690 | 1 | 0 | |a SPECIFICATION PATTERNS |
| 690 | 1 | 0 | |a SPECIFICATIONS |
| 700 | 1 | |a Braberman, V. | |
| 773 | 0 | |d World Scientific Publishing Co. Pte Ltd, 2015 |g v. 25 |h pp. 669-700 |k n. 4 |p Int. J. Software Engineer. Knowledge Engineer. |x 02181940 |t International Journal of Software Engineering and Knowledge Engineering | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84941918609&doi=10.1142%2fS0218194015500060&partnerID=40&md5=b32cf3c8e52c02c846ec6e9a55cfbce2 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1142/S0218194015500060 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_02181940_v25_n4_p669_Asteasuain |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02181940_v25_n4_p669_Asteasuain |y Registro en la Biblioteca Digital |
| 961 | |a paper_02181940_v25_n4_p669_Asteasuain |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 74786 | ||