Barnett, Mike, Edwards, Stephen H., Giannakopoulou, Dimitra, Leavens, Gary T. and Sharygina, Natasha (2005) SAVCBS 2005 Proceedings: Specification and Verification of Component-Based Systems. Technical Report 05-19, Computer Science, Iowa State University.
This workshop is concerned with how formal (i.e., mathematical) techniques can be or should be used to
establish a suitable foundation for the specification and verification of component-based systems.
Component-based systems are a growing concern for the software engineering community. Specification
and reasoning techniques are urgently needed to permit composition of systems from components.
Component-based specification and verification is also vital for scaling advanced verification techniques
such as extended static analysis and model checking to the size of real systems. The workshop will
consider formalization of both functional and non-functional behavior, such as performance or
This workshop brings together researchers and practitioners in the areas of component-based software
and formal methods to address the open problems in modular specification and verification of systems
composed from components. We are interested in bridging the gap between principles and practice. The
intent of bringing participants together at the workshop is to help form a community-oriented
understanding of the relevant research problems and help steer formal methods research in a direction
that will address the problems of component-based systems. For example, researchers in formal methods
have only recently begun to study principles of object-oriented software specification and verification,
but do not yet have a good handle on how inheritance can be exploited in specification and verification.
Other issues are also important in the practice of component-based systems, such as concurrency,
mechanization and scalability, performance (time and space), reusability, and understandability. The aim
is to brainstorm about these and related topics to understand both the problems involved and how formal
techniques may be useful in solving them.
|Keywords:||Specification, Verification, Component-Based Systems, static analysis, advanced type systems, model checking, composition, run-time assertion checking, JML language, performance specification, concurrency, |
|Subjects:||Software: PROGRAMMING TECHNIQUES (E): Concurrent Programming|
Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Coding Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Studies of Program Constructs (D.3.2-3)
|Deposited by:||Gary T. Leavens on 16 September 2005|
|Alternative Locations:||ftp://ftp.cs.iastate.edu/pub/techreports/TR05-19/TR.pdf |
Contact site administrator at: firstname.lastname@example.org