Specification patterns can be formal and still easy
Property specification is still one of the most challenging tasks for transference of software verification technology like model checking. 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 satis...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2010
|
| Acceso en línea: | Registro en Scopus Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 07599caa a22007217a 4500 | ||
|---|---|---|---|
| 001 | PAPER-7479 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203714.0 | ||
| 008 | 190411s2010 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-79952460289 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Asteasuain, F. | |
| 245 | 1 | 0 | |a Specification patterns can be formal and still easy |
| 260 | |c 2010 | ||
| 270 | 1 | 0 | |m Asteasuain, F.; FCEyN, University of Buenos AiresArgentina; email: fasteasuain@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Alfonso, A., Braberman, V., Kicillof, N., Olivero, A., Visual timed event scenarios (2004) Proceedings of the 26th International Conference on Software Engineering, p. 177. , IEEE Computer Society | ||
| 504 | |a Autili, M., Inverardi, P., Pelliccione, P., Graphical scenarios for specifying temporal properties: An automated approach (2007) Automated Software Engineering, 14 (3), pp. 293-340. , DOI 10.1007/s10515-007-0012-6 | ||
| 504 | |a Autili, M., Pelliccione, P., Towards a Graphical Tool for Refining User to System Requirements (2008) Electronic Notes in Theoretical Computer Science, 211 (C), pp. 147-157. , DOI 10.1016/j.entcs.2008.04.037, PII S1571066108002521 | ||
| 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, p. 72. , 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 Transactions on Software Engineering, 31 (12), pp. 1028-1041. , DOI 10.1109/TSE.2005.131 | ||
| 504 | |a Cobleigh, R., Avrunin, G., Clarke, L., User guidance for creating precise and accessible property specifications (2006) Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, p. 218. , ACM | ||
| 504 | |a Dillon, L., Kutty, G., Moser, L., Melliar-Smith, P., Ramakrishna, Y., A graphical interval logic for specifying concurrent systems (1994) ACM Transactions on Software Engineering and Methodology (TOSEM), 3 (2), pp. 131-165 | ||
| 504 | |a Dwyer, M., Avrunin, G., Corbett, J., Specification PatternsWeb Site, , http://patterns.projects.cis.ksu.edu/documentation/patterns.shtml | ||
| 504 | |a Dwyer, M., Avrunin, G., Corbett, J., Patterns in property specifications for finite-state verification (1999) Proceedings of the 21st International Conference on Software Engineering ICSE, 99 | ||
| 504 | |a Giannakopoulou, D., Magee, J., Fluent model checking for event based systems (2003) Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, p. 266. , ACM | ||
| 504 | |a Harel, D., Marelly, R., Playing with time: On the specification and execution of time-enriched lscs MASCOTS'02, pp. 193-202. , IEEE Computer Society | ||
| 504 | |a Holzmann, G., The logic of bugs (2002) ACM SIGSOFT Software Engineering Notes, 27 (6), p. 87 | ||
| 504 | |a Konrad, S., Cheng, B., Real-time specification patterns (2005) Proceedings of the 27th ICSE, pp. 372-381. , ACM | ||
| 504 | |a Laroussinie, F., Markey, N., Schnoebelen, P., Temporal logic with forgettable past (2002) Proceedings-Symposium on Logic in Computer Science, pp. 383-392. , 2002 | ||
| 504 | |a Markey, N., Temporal logic with past is exponentially more succinct (2003) EATCS Bull, 79, pp. 122-128 | ||
| 504 | |a Paun, D., Chechik, M., Events in linear-time properties (1999) Proceedings of 4th International Conference on Requirements Engineering, , Citeseer | ||
| 504 | |a Pradella, M., Pietro, P.S., Spoletini, P., Morzenti, A., Practical model checking of LTL with past (2003) ATVA03: 1st Workshop on Automated Technology for Verification and Analysis, , Citeseer | ||
| 504 | |a Viggers, R.W.R., Viggers, K., Implementing protocols via declarative event patterns (2004) ACM Sigsoft International Symposium on FSE(FSE-12), pp. 158-169 | ||
| 504 | |a Sengupta, B., Cleaveland, R., Triggered message sequence charts (2002) SIGSOFT FSE, pp. 167-176 | ||
| 504 | |a Smith, M.H., Holzmann, G.J., Etessami, K., Events and constraints: A graphical editor for capturing logic requirements of programs (2001) Proceedings of the IEEE International Conference on Requirements Engineering, pp. 14-22 | ||
| 504 | |a Smith, R.L., Avrunin, G.S., Clarke, L.A., Osterweil, L.J., PROPEL: An approach supporting property elucidation (2002) Proceedings - International Conference on Software Engineering, pp. 11-21 | ||
| 504 | |a Uchitel, S., Kramer, J., Magee, J., Negative scenarios for implied scenario elicitation (2002) Proc. of FSE'02, pp. 109-118. , ACM PressA4 - Knowledge Systems Institute Graduate School | ||
| 520 | 3 | |a Property specification is still one of the most challenging tasks for transference of software verification technology like model checking. 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 pattern the developer may have to deal with the pattern expressed in some particular formalism. For this reason, we identify three desirable quality attributes for the underlying specification language: succinctness, ease of validation and modifiability. We show that typical formalisms such as temporal logics or automata fail at some extent to support these features. In this work we propose FVS, a graphical scenario-based language, as a possible alternative to specify behavioral properties. We illustrate FVS' features by describing one of the most commonly used pattern, the Response Pattern, and several variants of it. Other known patterns such as the Precedence pattern and the Constrained Chain pattern are also discussed. We also thoroughly compare FVS against other used approaches. |l eng | |
| 593 | |a FCEyN, University of Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a BEHAVIORAL PROPERTIES |
| 690 | 1 | 0 | |a MODIFIABILITY |
| 690 | 1 | 0 | |a PROPERTY SPECIFICATION |
| 690 | 1 | 0 | |a QUALITY ATTRIBUTES |
| 690 | 1 | 0 | |a RESPONSE PATTERNS |
| 690 | 1 | 0 | |a SCENARIO-BASED LANGUAGES |
| 690 | 1 | 0 | |a SOFTWARE VERIFICATION |
| 690 | 1 | 0 | |a SPECIFICATION PATTERNS |
| 690 | 1 | 0 | |a FORMAL LANGUAGES |
| 690 | 1 | 0 | |a KNOWLEDGE ENGINEERING |
| 690 | 1 | 0 | |a SOFTWARE ENGINEERING |
| 690 | 1 | 0 | |a SPECIFICATION LANGUAGES |
| 690 | 1 | 0 | |a SPECIFICATIONS |
| 690 | 1 | 0 | |a MODEL CHECKING |
| 700 | 1 | |a Braberman, V. | |
| 711 | 2 | |c Redwood City, CA |d 1 July 2010 through 3 July 2010 |g Código de la conferencia: 84044 | |
| 773 | 0 | |d 2010 |h pp. 430-436 |p SEKE - Proc. Int. Conf. Softw. Eng. Knowl. Eng. |n SEKE 2010 - Proceedings of the 22nd International Conference on Software Engineering and Knowledge Engineering |z 1891706268 |z 9781891706264 |t 22nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2010 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-79952460289&partnerID=40&md5=dad31ac887a90cfde103af2badb434a8 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_18917062_v_n_p430_Asteasuain |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_18917062_v_n_p430_Asteasuain |y Registro en la Biblioteca Digital |
| 961 | |a paper_18917062_v_n_p430_Asteasuain |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 68432 | ||