Declaratively building behavior by means of scenario clauses

Behavior needs to be understood from early stages of software development. In this context, incremental and declarative modeling seems an attractive approach for closely capturing and analyzing requirements without early operational commitment. A traditional choice for such a kind of modeling is a l...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Asteasuain, F.
Otros Autores: Braberman, V.
Formato: Capítulo de libro
Lenguaje:Inglés
Publicado: Springer London 2017
Acceso en línea:Registro en Scopus
DOI
Handle
Registro en la Biblioteca Digital
Aporte de:Registro referencial: Solicitar el recurso aquí
LEADER 13195caa a22012017a 4500
001 PAPER-14958
003 AR-BaUEN
005 20230518204534.0
008 190410s2017 xx ||||fo|||| 00| 0 eng|d
024 7 |2 scopus  |a 2-s2.0-84954429676 
040 |a Scopus  |b spa  |c AR-BaUEN  |d AR-BaUEN 
100 1 |a Asteasuain, F. 
245 1 0 |a Declaratively building behavior by means of scenario clauses 
260 |b Springer London  |c 2017 
270 1 0 |m Asteasuain, F.; Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Pabellon I, Ciudad Universitaria, Argentina; 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) In: 26th ICSE’04 
504 |a Areces, C., Hoffmann, G., Denis A (2010) Modal logics with counting 17th workshop on logic, language, information and computation, Brazil. Springer, pp. 98-109. , Berlin, Heidelberg 
504 |a Asteasuain, F., Braberman, V., Specification patterns can be formal and also easy (2010) In: The 22nd international conference on software engineering and knowledge engineering (SEKE) 
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) Electronic notes in theoretical computer science (ENTCS), 211, pp. 147-157 
504 |a Bianculli, D., Ghezzi, C., Pautasso, C., Senti, P., Specification patterns from research to industry: a case study in service-based applications (2012) In: Proceedings of the 2012 international conference on software engineering. IEEE Press 
504 |a Bloem, R., Cavada, R., Eisner, C., Pill, I., Roveri, M., Semprini, S., Manual for property simulation and assurance tool (deliverable 1.2/4–5) (2004) In: Technical report, , PROSYD Project, Technical Report 
504 |a Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O., Temporal specifications with accumulative values. In: 26th annual IEEE symposium on logic in computer science (LICS) (2011) IEEE 
504 |a Bosscher, D., Polak, I., Vaandrager F (1994) Verification of an audio control protocol Formal techniques in real-time and fault-tolerant systems. Springer, pp. 170-192. , Berlin, Heidelberg 
504 |a Bouajjani, A., Lakhnech, Y., Yovine S (1996) Model checking for extended timed temporal logics Formal techniques in real-time and fault-tolerant systems. Springer, pp. 306-326. , Berlin, Heidelberg 
504 |a Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero A (2009) Speeding up model checking of timed-models by combining scenario specialization and live component analysis Formal modeling and analysis of timed systems. Springer, pp. 58-72. , Berlin, Heidelberg 
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, , Springer, New York 
504 |a Buchi online Store, , http://buchi.im.ntu.edu.tw/index.php/browse/index/ 
504 |a Cobleigh, R., Avrunin, G., Clarke, L., User guidance for creating precise and accessible property specifications (2006) In: Proceedings of the 14th ACM SIGSOFT international symposium on foundations of software engineering. ACM 
504 |a Dalal, S., Jain, A., Karunanithi, N., Leaton, J., Lott, C., Patton, G., Horowitz, B., Model-based testing in practice (1999) In: Proceedings of the 21st international conference on software engineering. ACM 
504 |a David, S., Orni, A., (2005) Property-by-example guide: a handbook of psl/sugar examples-prosyd deliverable d1 
504 |a De Alfaro, L., Henzinger, T., Interface automata (2001) ACM SIGSOFT Softw Eng Notes, 26 (5), p. 120 
504 |a Dillon, L., Kutty, G., Moser, L., Melliar-Smith, P., Ramakrishna, Y., A graphical interval logic for specifying concurrent systems (1994) ACM Trans Softw Eng Methodol (TOSEM), 3 (2), pp. 131-165 
504 |a D’Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., Synthesis of live behaviour models. In: Proceedings of the 18th ACM SIGSOFT international symposium on foundations of software engineering (2010) ACM SIGSOFT 
504 |a Specification Patterns Web Site, , http://patterns.projects.cis.ksu.edu/documentation/patterns.shtml, Dwyer M, Avrunin G, Corbett J In 
504 |a Dwyer, M., Avrunin, G., Corbett, J., Patterns in property specifications for finite-state verification (1999) In: Proceedings of the 21st international conference on software engineering ICSE 
504 |a Eisner, C., Fisman, D., (2006) A practical introduction to PSL (series on integrated circuits and systems), , Springer, Secaucus 
504 |a Fritz, C., Wilke, T., State space reductions for alternating büchi automata quotienting by simulation equivalences (2002) In: FST TCS 2002: foundations of software technology and theoretical computer science. Springer 
504 |a Gary, M.R., Johnson, D.S., (1979) Computers and intractability: a guide to the theory of np-completeness, , Freeman and Company, San Francisco 
504 |a Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) In: Proceedings of the 9th European software engineering conference. ACM 
504 |a Playing with time: On the specification and execution of time-enriched lscs In: MASCOTS ’02. IEEE computer society, , Harel D, Marelly R pp 193–202 
504 |a Holzmann, G., The logic of bugs (2002) ACM Softw Eng Notes, 27 (6), p. 87 
504 |a Konrad, S., Cheng, B., Real-time specification patterns (2005) In: Proceedings of the 27th ICSE. ACM 
504 |a Kupferman, O., Piterman, N., Vardi, M., Extended temporal logic revisited (2001) In: CONCUR 2001 concurrency theory 
504 |a Lamsweerde, A.V., Goal-oriented requirements engineering: a guided tour (2001) In: RE’01—international joint conference on RE 
504 |a (1993) RFC1508: generic security service application program interface RFC Editor United States, , Linn J 
504 |a Luckham, D., (2011) Event processing for business: organizing the real-time enterprise, , Wiley, Hoboken 
504 |a McCarthy, J., Hayes, P., Some philosophical problems from the standpoint of artificial intelligence (1968) Stanford University 
504 |a (2008) NET NegotiateStream Protocol Specification v2.0., , http://msdn.microsoft.com/en-us/library/cc236723.aspx, [MS-NNS] July 
504 |a Noda, N., Kishi, T., An aspect-oriented modeling mechanism based on state diagrams (2006) In: 9th international workshop on AOM 
504 |a Pelov, N., Denecker, M., Bruynooghe, M., Well-founded and stable semantics of logic programs with aggregates (2007) Theory Pract Logic Program, 7 (3), p. 301 
504 |a Piterman, N., Pnueli, A., Sa’ar, Y., Synthesis of reactive (1) designs (2006) Lecture notes in computer science, 3855, p. 364 
504 |a Pnueli, A., The temporal logic of programs (1977) In: 18th annual symposium on foundations of computer science, 1977. IEEE 
504 |a Pnueli, A., Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends (1986) Current trends in Concurrency, pp. 510-584 
504 |a Post, A., Hoenicke, J., Formalization and analysis of real-time requirements: a feasibility study at bosch (2012) In: VSTTE 
504 |a Post, A., Menzel, I., Hoenicke, J., Podelski, A., Automotive behavioral requirements expressed in a specification pattern system: a case study at bosch (2012) Requir Eng, 17 (1), pp. 19-33 
504 |a Implementing protocols via declarative event patterns. (2004) In: ACM sigsoft international symposium on FSE (FSE-12) 
504 |a Sánchez, C., Leucker, M., Regular linear temporal logic with past (2010) In: Verification, model checking, and abstract interpretation. Springer 
504 |a Sengupta, B., Cleaveland, R., Triggered message sequence charts (2002) In: SIGSOFT FSE 
504 |a Sibay, G., Uchitel, S., Braberman, V., Existential live sequence charts revisited (2008) In: Proceedings of ICSE. ACM New York 
504 |a Smith, M., Holzmann, G., Etessami, K., Events and constraints: a graphical editor for capturing logic requirements of programs (2001) In: Proceedings of fifth IEEE international symposium on requirements engineering, 2001. IEEE 
504 |a Smith, R., Avrunin, G., Clarke, L., Osterweil, L., Propel: an approach supporting property elucidation (2002) ICSE, 24, pp. 11-21 
504 |a Somenzi, F., Bloem, R., Efficient büchi automata from ltl formulae (2000) In: Computer aided verification. Springer 
504 |a Tsay, Y., Chen, Y., Tsai, M., Wu, K., Chan, W., Goal: A graphical tool for manipulating büchi automata and temporal formulae (2007) In: Tools and algorithms for the construction and analysis of systems 
504 |a Tsay, Y., Tsai, M., Chang, J., Chang, Y., Büchi store: an open repository of büchi automata (2011) In: Tools and algorithms for the construction and analysis of systems pp 262–266 
504 |a Uchitel, S., Kramer, J., Magee, J., Negative scenarios for implied scenario elicitation (2002) In: Proceedings of FSE ’02. ACM Press 
504 |a Utting, M., Legeard, B., (2007) Practical model-based testing: a tools approach, , Morgan Kaufmann, San Francisco 
504 |a Van Harmelen, F., Lifschitz, V., Porter, B., (2008) Handbook of knowledge representation, , 1, Elsevier Science, San Diego 
504 |a (1994) Reasoning about infinite computations, , Vardiy M, Wolperz P 
504 |a Veanes, M., Schulte, W., Protocol modeling with model program composition (2008) Lecture notes in computer science, 5048, p. 324 
504 |a Wolper, P., Temporal logic can be more expressive (1983) Inf Control, 56 (1-2), pp. 72-99 
504 |a Wolper, P., Vardi, M., Sistla, A., Reasoning about infinite computation paths (1983) In: 24th annual symposium on foundations of computer science, 1983. IEEE 
504 |a Wu, Z., On the expressive power of qltl (2007) In: Proceedings of the 4th international conference on theoretical aspects of computing. Springer 
520 3 |a Behavior needs to be understood from early stages of software development. In this context, incremental and declarative modeling seems an attractive approach for closely capturing and analyzing requirements without early operational commitment. A traditional choice for such a kind of modeling is a logic-based approach. Unfortunately, in many cases, the formal description and validation of properties result in a daunting task, even for trained people. Moreover, some authors established some practical limitations with temporal logics expressive power. In this work, we present omega-feather weight visual scenarios (ω-FVS) a declarative language, not founded on temporal logics, but on simple graphical scenarios, powerful enough to express ω-regular properties. The notation is equipped with declarative semantics based on morphisms, and a tableau procedure is given enabling the possibility of automatic analysis. © 2016, Springer-Verlag London.  |l eng 
593 |a Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Pabellon I, Ciudad Universitaria, Buenos Aires, C1428EGA, Argentina 
593 |a Ing. en Informática, Departamento de Tecnología y Administración, Universidad Nacional de Avellaneda, Mario Bravo 1460, Piñeyro, Buenos Aires, 1870, Argentina 
690 1 0 |a BEHAVIORAL MODELING 
690 1 0 |a FORMAL SPECIFICATIONS 
690 1 0 |a REQUIREMENTS ENGINEERING 
690 1 0 |a FORMAL SPECIFICATION 
690 1 0 |a REQUIREMENTS ENGINEERING 
690 1 0 |a SEMANTICS 
690 1 0 |a TEMPORAL LOGIC 
690 1 0 |a BEHAVIORAL MODEL 
690 1 0 |a DECLARATIVE LANGUAGES 
690 1 0 |a DECLARATIVE MODELS 
690 1 0 |a DECLARATIVE SEMANTICS 
690 1 0 |a FORMAL DESCRIPTION 
690 1 0 |a LOGIC-BASED APPROACH 
690 1 0 |a OPERATIONAL COMMITMENTS 
690 1 0 |a REGULAR PROPERTIES 
690 1 0 |a SOFTWARE DESIGN 
700 1 |a Braberman, V. 
773 0 |d Springer London, 2017  |g v. 22  |h pp. 239-274  |k n. 2  |p Requir. Eng.  |x 09473602  |t Requirements Engineering 
856 4 1 |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84954429676&doi=10.1007%2fs00766-015-0242-2&partnerID=40&md5=fe485cd64080fdc06ea239bd7b7a8593  |y Registro en Scopus 
856 4 0 |u https://doi.org/10.1007/s00766-015-0242-2  |y DOI 
856 4 0 |u https://hdl.handle.net/20.500.12110/paper_09473602_v22_n2_p239_Asteasuain  |y Handle 
856 4 0 |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09473602_v22_n2_p239_Asteasuain  |y Registro en la Biblioteca Digital 
961 |a paper_09473602_v22_n2_p239_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 75911