- -

Graph generation to statically represent CSP processes

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Graph generation to statically represent CSP processes

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: paper8-ProcLOPSTR ...
Tamaño: 406.9Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Graph Generation ...
Tamaño: 310.0Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Llorens Agost, María Luisa es_ES
dc.contributor.author Oliver Villarroya, Javier es_ES
dc.contributor.author Silva Galiana, Josep Francesc es_ES
dc.contributor.author Tamarit Muñoz, Salvador es_ES
dc.date.accessioned 2014-03-03T11:45:17Z
dc.date.issued 2011
dc.identifier.isbn 978-3-642-20550-7
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/10251/36090
dc.description.abstract The CSP language allows the specification and verification of complex concurrent systems. Many analyses for CSP exist that have been successfully applied in different industrial projects. However, the cost of the analyses performed is usually very high, and sometimes prohibitive, due to the complexity imposed by the non-deterministic execution order of processes and to the restrictions imposed on this order by synchronizations. In this work, we define a data structure that allows us to statically simplify a specification before the analyses. This simplification can drastically reduce the time needed by many CSP analyses. We also introduce an algorithm able to automatically generate this data structure from a CSP specification. The algorithm has been proved correct and its implementation for the CSP's animator ProB is publicly available. © 2011 Springer-Verlag. es_ES
dc.description.sponsorship This work has been partially supported by the Spanish Ministerio de Ciencia e Innovación under grant TIN2008-06622-C03-02, by the Generalitat Valenciana under grant ACOMP/2010/042, and by the Universidad Politécnica de Valencia (Program PAID-06-08). Salvador Tamarit was partially supported by the Spanish MICINN under FPI grant BES-2009-015019. es_ES
dc.format.extent 15 es_ES
dc.language Inglés es_ES
dc.publisher Springer Verlag (Germany) es_ES
dc.relation.ispartof Logic-Based Program Synthesis and Transformation es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;vol. 6564
dc.rights Reserva de todos los derechos es_ES
dc.subject Complex concurrent systems es_ES
dc.subject CSP specifications es_ES
dc.subject Deterministic execution es_ES
dc.subject Graph generation es_ES
dc.subject Industrial projects es_ES
dc.subject Specification and verification es_ES
dc.subject Algorithms es_ES
dc.subject Animation es_ES
dc.subject Data structures es_ES
dc.subject Logic programming es_ES
dc.subject Specifications es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Graph generation to statically represent CSP processes es_ES
dc.type Capítulo de libro es_ES
dc.embargo.lift 10000-01-01
dc.embargo.terms forever es_ES
dc.identifier.doi 10.1007/978-3-642-20551-4_4
dc.relation.projectID info:eu-repo/grantAgreement/MICINN//TIN2008-06622-C03-02/ES/VERIFICACION Y DEPURACION AGILES ORIENTADAS A MEJORAR LA SEGURIDAD DEL SOFTWARE/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//ACOMP%2F2010%2F042/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/UPV//PAID-06-08/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MICINN//BES-2009-015019/ES/BES-2009-015019/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Llorens Agost, ML.; Oliver Villarroya, J.; Silva Galiana, JF.; Tamarit Muñoz, S. (2011). Graph generation to statically represent CSP processes. En Logic-Based Program Synthesis and Transformation. Springer Verlag (Germany). 6564:52-66. https://doi.org/10.1007/978-3-642-20551-4_4 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 20th International Symposium, LOPSTR 2010 es_ES
dc.relation.conferencedate July 23-25, 2010 es_ES
dc.relation.conferenceplace Hagenberg, Austria es_ES
dc.relation.publisherversion http://link.springer.com/chapter/10.1007/978-3-642-20551-4_4 es_ES
dc.description.upvformatpinicio 52 es_ES
dc.description.upvformatpfin 66 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 6564 es_ES
dc.relation.senia 213129
dc.contributor.funder Ministerio de Ciencia e Innovación es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Universitat Politècnica de València es_ES
dc.description.references Brassel, B., Hanus, M., Huch, F., Vidal, G.: A Semantics for Tracing Declarative Multi-paradigm Programs. In: Moggi, E., Warren, D.S. (eds.) 6th ACM SIGPLAN Int’l Conf. on Principles and Practice of Declarative Programming (PPDP 2004), pp. 179–190. ACM, New York (2004) es_ES
dc.description.references Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005) es_ES
dc.description.references Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985) es_ES
dc.description.references Kavi, K.M., Sheldon, F.T., Shirazi, B., Hurson, A.R.: Reliability Analysis of CSP Specifications using Petri Nets and Markov Processes. In: 28th Annual Hawaii Int’l Conf. on System Sciences (HICSS 1995). Software Technology, vol. 2, pp. 516–524. IEEE Computer Society, Washington, DC, USA (1995) es_ES
dc.description.references Ladkin, P., Simons, B.: Static Deadlock Analysis for CSP-Type Communications. In: Responsive Computer Systems (Ch. 5). Kluwer Academic Publishers, Dordrecht (1995) es_ES
dc.description.references Leuschel, M., Butler, M.: ProB: an Automated Analysis Toolset for the B Method. Journal of Software Tools for Technology Transfer 10(2), 185–203 (2008) es_ES
dc.description.references Leuschel, M., Llorens, M., Oliver, J., Silva, J., Tamarit, S.: Static Slicing of CSP Specifications. In: Hanus, M. (ed.) 18th Int’l Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR 2008), pp. 141–150. Technical report, DSIC-II/09/08, Universidad Politécnica de Valencia (July 2008) es_ES
dc.description.references Leuschel, M., Llorens, M., Oliver, J., Silva, J., Tamarit, S.: SOC: a Slicer for CSP Specifications. In: Puebla, G., Vidal, G. (eds.) 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM 2009), pp. 165–168. ACM, New York (2009) es_ES
dc.description.references Leuschel, M., Llorens, M., Oliver, J., Silva, J., Tamarit, S.: The MEB and CEB static analysis for CSP specifications. In: Hanus, M. (ed.) LOPSTR 2008. LNCS, vol. 5438, pp. 103–118. Springer, Heidelberg (2009) es_ES
dc.description.references Llorens, M., Oliver, J., Silva, J., Tamarit, S.: A Semantics to Generate the Context-sensitive Synchronized Control-Flow Graph (extended). Technical report DSIC, Universidad Politécnica de Valencia, Valencia, Spain (June 2010), http://www.dsic.upv.es/~jsilva es_ES
dc.description.references Llorens, M., Oliver, J., Silva, J., Tamarit, S.: Transforming Communicating Sequential Processes to Petri Nets. In: Topping, B.H.V., Adam, J.M., Pallarés, F.J., Bru, R., Romero, M.L. (eds.) Seventh Int’l Conference on Engineering Computational Technology (ICECT 2010). Civil-Comp Press, Stirlingshire, UK, Paper 26 (2010) es_ES
dc.description.references Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, Heidelberg (1995) es_ES
dc.description.references Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (2005) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem