PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bracciali A., Brogi A., Turini F. A framework for specifying and verifying the behaviour of open systems. In: Journal of Logic and Algebraic Programming, vol. 63 (2) pp. 215 - 240. Special Issue: Process Algebra and System Architecture. Elsevier, 2005.
 
 
Abstract
(English)
Coding no longer represents the main issue in developing software applications. It is the design and verification of complex software systems that require to be addressed at the architectural level, following methodologies which permit us to clearly identify and design the components of a system, to understand precisely their interactions, and to formally verify the properties of the systems. Moreover, this process is made even more complicated by the advent of the "network-centric" model of computation, where open systems dynamically interact with each other in a highly volatile environment. Many of the techniques traditionally used for closed systems are inadequate in this context. We illustrate how the problem of modeling and verifying behavioural properties of open system is addressed by different research fields and how their results may contribute to a common solution. Building on this, we propose a methodology for modeling and verifying behavioural aspects of open systems. We introduce the IP-calculus, derived from the π-calculas process algebra so as to describe behavioural features of open systems. We define a notion of partial correctness, acceptability, in order to deal with the intrinsic indeterminacy of open systems, and we provide an algorithmic procedure for its effective verification.
URL: http://www.sciencedirect.com/science/article/pii/S1567832604000372
DOI: 10.1016/j.jlap.2004.05.004
Subject Open systems
Process algebras
Verification
H.3.4 Systems and Software


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional