Formal Methods
|
Introduction
Our work in the field of formal methods focuses on analysis of source code (Java, C/C++) as well as on model checking of behavior specification of software components (SOFA, Fractal) in the form of Behavior Protocols and their extensions. For more information, please refer to the following paragraphs.
Members
| Name |
Contact |
Research topics |
|
David Hauzar |
+420 221 914 121
|
code model checking
verification of web applications |
|
Pavel Jančík |
+420 221 914 121
|
code model checking |
|
Jan Kofroň Group leader
|
+420 221 914 285
|
formal verification
code model checking |
|
Pavel Parízek |
+420 221 914 235 currently on postdoc
|
behavior modeling and verification of software components
automated verification and analysis of programs |
|
František Plášil |
+420 221 914 266
|
component-based programming, SOA
behavior specification and verification, model checking
object-oriented and distributed systems |
|
Ondřej Šerý |
+420 221 914 285
|
behavior specification of software components and code analysis |
Code Analysis
Our work in code analysis focuses on checking whether implementation of
a component satisfies the behavior specification in behavior protocols.
We have developed two checking techniques, which are based on program
model checking – one for components in Java and the other for components
in C. For checking of Java components, we use the Java PathFinder model
checker and extend it in various ways to make checking of code against
behavior protocols possible. The BLAST model checker with a behavior
specification extension is used for analysis of C programs. In cooperation
with ABB Germany, we have conducted a case study on analysis of the C
implementation of the OPC-UA stack.
We also develop an explicit code model checker for C/C++, called GMC. For more information on this project, please refer to the GMC homepage
Behavior Modeling
In the area of behavior modeling, we focus on specification of component
behavior as observable from outside, i. e., a black-box view, and
verification of the following goals:
- Suitable modeling abstractions –
we aim at providing a behavior specification formalism being
a good balance between expressiveness and simplicity w.r.t. automatic analysis.
- Tool-supported automated verification –
the goal is to provide tools for automatic verification of correctness of components'
composition (i. e., a set of components communicates without errors) and
components' substitutability (i. e., a component can be safely substituted
by another one).
Starting with Behavior Protocols (BP) – a simple process algebra reflecting
just sequencies of method calls on component frame (the set of component provided
and required interfaces), we enriched the formalism with methods parameters and
local variables (Extended Behavior Protocols – EBP) and later also with threads
(Threaded Behavior Protocol – TBP).
Reverse Engineering
Providing behavior models for our methods by hand is demanding and error
prone and is considered as one of the major obstacles when applying our methods
in practice. Especially in context of legacy applications, when source code of
individual components is available, automatic approach can be used to analyze
important aspects of component behavior already present in the code and capture
it by means of TBP formalism.
Research Frameworks
- CREF – Component Reliability Extension for Fractal Component Model
- CoCoME – Common Component Modeling Environment is evaluation
and comparison of the practical appliance
of existing component models using a common
component-based system as modelling example
- Behavior protocols in Fractal – Extending the Fractal component model and its Julia
implementation with support for behavior protocols
- Behavior protocols in SOFA – Specification of component behavior in a process-algebra like manner
- Q-ImPrESS (FP7 STREP) – Quality Impact Prediction for Evolving Service-oriented Software
- ASCENS (FP7 FET IP) – Autonomic Service-Component Ensembles
Software and Tools
- BPEL checker – Checker of BPEL code against behavior protocols
- BLAST Extension – Behavior analysis extension of the BLAST model checker
- Carmen – Software component model checker for Fractal
- COMBAT – Component Behavior Analysis Toolset
- dChecker – Distributed checker of behavior protocols (with behavior protocol slicing extension BPSlicer)
- EnvGen – ENVironment GENerator for Java PathFinder
- JAbstractor – Extracting TBP specification from the Java implementation of a primitive component
- Procasor – Deriving behavior specifications from textual use cases
- ReProTool – Requirements Processing Tool
- BeJC – Behavior Java Checker
- Gimple Model Checker – Model checker of the Gimple intermediate code produced by the gcc compiler
Publications
2011 (2)
Technical Reports
Nonrefereed
2010 (8)
Refereed (journals/proceedings)
| PDF |
Parízek P., Yuldashev N.: Extraction of Component-Environment Interaction Model Using State Space Traversal,
In Proceedings of the 25th ACM Symposium on Applied Computing (SAC 2010), SE track, ACM, March 2010 |
| PDF |
Parízek P., Plášil F.: Assume-Guarantee Verification of Software Components in SOFA 2 Framework,
In IET Software, volume 4, issue 3, ISSN 1751-8806, June 2010 |
| PDF |
Kolb E., Šerý O., Weiss R.: Applicability of the BLAST Model Checker: An Industrial Case Study,
In Proceedings of PSI'09, LNCS 5947, ISBN 978-3-642-11485-4, pp. 218-229, January 2010 |
| Link |
Becker S., Hauck M., Trifu M., Krogmann K., Kofroň J.: Reverse Engineering Component Models for Quality Predictions,
in Proceedings of the 14th
European Conference on Software Maintenance and Reengineering,
European Projects Track, (c) IEEE, ISBN: 978-0-7695-4321-5, March 2010
(preliminary version available here)
|
| PDF, Link |
Babka V., Tůma P., Bulej L.: Validating Model-Driven Performance Predictions On Random Software Systems,
In the Proceedings of the Sixth International Conference on the Quality of Software Architectures (QoSA 2010, federate event of CompArch 2010), Springer-Verlag, LNCS 6093, ISBN 978-3-642-13820-1, ISSN 0302-9743, pp. 3-19, June 2010 |
Ph.D. Theses
| PDF |
Šerý O.: Automated Verification of Software,
Ph.D. thesis, advisor: Frantisek Plasil, September 2010 |
| PDF |
Poch T.: Towards Thread Aware Component Specifications,
Ph.D. thesis, advisor: Frantisek Plasil, September 2010 |
Technical Reports
| PDF |
Babka V., Bulej L., Ciancone A., Filieri A., Hauck M., Libič P., Marek L., Stammel J., Tůma P.: Prediction Validation,
Q-ImPrESS Project Deliverable D4.2, July 2010 |
2009 (9)
Refereed (journals/proceedings)
| PDF, Link |
Babka V., Tůma P.: Investigating Cache Parameters of x86 Family Processors,
In Proceedings of SPEC Benchmark Workshop 2009, Austin, TX, USA, Awarded with Kaivalya Dixit Award. Springer-Verlag, LNCS 5419, ISBN 978-3-540-93798-2, ISSN 0302-9743, pp. 77-96, January 2009 |
| PDF |
Šerý O.: Enhanced Property Specification and Verification in BLAST,
In Proceedings of FASE 2009, LNCS 5503, pp. 456-469, York, UK, March 2009 |
| PDF, Link |
Libič P., Tůma P., Bulej L.: Issues in Performance Modeling of Applications with Garbage Collection,
In Proceedings of QUASOSS 2009, Amsterdam, Netherlands, ACM, ISBN 978-1-60558-709-7, pp. 3-10, August 2009 |
| PDF, PDF, Link |
Babka V., Libič P., Tůma P.: Timing Penalties Associated with Cache Sharing,
In Proceedings of MASCOTS 2009, London, UK, IEEE, ISBN: 978-1-4244-4926-2, ISSN: 1526-7539, pp. 583-586, September 2009 |
| PDF |
Kofroň J., Poch T., Šerý O.: TBP: Code-Oriented Component Behavior Specification,
In Proceedings of SEW-32, IEEE, ISBN 978-0-7695-3617-0, pp. 75-83, Greece, January 2009 |
| PDF |
Kebrt M., Šerý O.: UnitCheck: Unit Testing and Model Checking Combined,
In Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), LNCS 5799, ISBN 978-3-642-04760-2, pp. 97-103, October 2009 |
| PDF, Link |
Babka V., Marek L., Tůma P.: When Misses Differ: Investigating Impact of Cache Misses on Observed Performance,
In Proceedings of ICPADS 2009, Shenzhen, China, IEEE, ISBN: 978-0-7695-3900-3, ISSN: 1521-9097, pp. 112-119, December 2009 |
Technical Reports
| PDF |
Bulej L., Marek L., Tůma P.: Object Instance Profiling,
Tech. Report No. 2009/7, Dep. of SW Engineering, Charles University in Prague, November 2009 |
Master Theses
| PDF |
Marek L.: Parallel Processing and Software Performance,
Master thesis, advisor: Petr Tuma, January 2009 |
2008 (8)
Refereed (journals/proceedings)
| PDF |
Bureš T., Děcký M., Hnětynka P., Kofroň J., Parízek P., Plášil F., Poch T., Šerý O., Tůma P.: CoCoME in SOFA,
Chapter in The Common Component Modeling Example: Comparing Software Component Models, Springer-Verlag, LNCS 5153, August 2008 |
| PDF, Link |
Parízek P., Plášil F.: Modeling of Component Environment in Presence of Callbacks and Autonomous Activities,
In Proceedings of TOOLS EUROPE 2008, Springer-Verlag, LNBIP, vol. 11, ISBN 3-540-69823-4, ISSN 1865-1348, pp. 2-21, June 2008 |
| PDF |
Plšek A., Adámek J.: Carmen: Software Component Model Checker,
in Proceedings of QoSA 2008, Karlsruhe, Germany, Springer, LNCS 5281, ISBN 978-3-540-87878-0, ISSN 0302-9743, pp. 71-85, October 2008 |
| PDF, Link |
Parízek P., Adámek J.: Checking Session-Oriented Interactions between Web Services,
In Proceedings of 34th EUROMICRO SEAA conference, IEEE Computer Society, ISBN 978-0-7695-3276-9, pp. 3-10, September 2008 |
| PDF |
Bulej L., Bureš T., Coupaye T., Děcký M., Ježek P., Parízek P., Plášil F., Poch T., Rivierre N., Šerý O., Tůma P.: CoCoME in Fractal,
Chapter in The Common Component Modeling Example: Comparing Software Component Models, Springer-Verlag, LNCS 5153, August 2008 |
Ph.D. Theses
| PDF |
Parízek P.: Formal Verification of Components in Java,
Ph.D. thesis, advisor: Frantisek Plasil, September 2008 |
Technical Reports
| PDF |
Parízek P., Adámek J.: Modeling and Verification of Session-Oriented Interactions between Web Services: Compliance of BPEL with Session Protocols,
Tech. Report No. 2008/2, Dep. of SW Engineering, Charles University in Prague, January 2008 |
| PDF |
Babka V., Bulej L., Děcký M., Kraft J., Libič P., Marek L., Seceleanu C., Tůma P.: Resource Usage Modeling,
Q-ImPrESS Project Deliverable D3.3, September 2008 |
2007 (10)
Refereed (journals/proceedings)
| PDF, Link |
Drazan J., Mencl V.: Improved Processing of Textual Use Cases: Deriving Behavior Specifications,
in Proceedings of SOFSEM 2007, January 20 - 26, 2007, Harrachov, Czech Republic, LNCS 4362, pp.856-868, DOI: 10.1007/978-3-540-69507-3_74, Springer, January 2007 |
| PDF, Link |
Parízek P., Plášil F., Kofroň J.: Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker,
In Proceedings of 30th IEEE/NASA Software Engineering Workshop (SEW-30), IEEE Computer Society, ISBN 0-7695-2624-1, ISSN 1550-6215, pp. 133-141, January 2007 |
| PDF, Link |
Parízek P., Plášil F.: Partial Verification of Software Components: Heuristics for Environment Construction,
In Proceedings of 33rd EUROMICRO SEAA conference, IEEE Computer Society, ISBN 0-7695-2977-1, ISSN 1089-6503, pp. 75-82, August 2007 |
| PDF, Link |
Parízek P., Plášil F.: Specification and Generation of Environment for Model Checking of Software Components,
In Proceedings of International Workshop on Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2006), ENTCS, Vol. 176, Issue 2, ISSN 1571-0661, pp. 143-154, May 2007 |
| PDF |
Šerý O., Plášil F.: Slicing of Component Behavior Specification with Respect to Their Composition,
In Proceedings of 10th International ACM SIGSOFT Symposium on Component-Based Software Engineering (CBSE 2007), LNCS 4608, July 2007 |
| PDF, Link |
Parízek P., Plášil F.: Modeling Environment for Component Model Checking from Hierarchical Architecture,
In Proceedings of Formal Aspects of Component Software (FACS'06), ENTCS, Vol. 182, ISSN 1571-0661, pp. 139-153, June 2007 |
Technical Reports
| PDF |
Parízek P., Plášil F.: Heuristic Reduction of Parallelism in Component Environment,
Tech. Report No. 2007/2, Dep. of SW Engineering, Charles University in Prague, March 2007 |
| PDF |
Šerý O., Plášil F.: Slicing behavior specification of components,
Tech. Report No. 2007/1, Dep. of SW Engineering, Charles University in Prague, January 2007 |
Nonrefereed
| PDF |
Bureš T., Děcký M., Hnětynka P., Kofroň J., Parízek P., Plášil F., Poch T., Šerý O., Tůma P.: CoCoME in SOFA 2.0,
Poster, Intel 12th EMEA Academic Forum, Intel Corporation, 2200 Mission College Blvd., Santa Clara, CA, USA, June 2007 |
| PDF |
Babka V., Děcký M., Tůma P.: Performance in CoCoME,
Poster, Intel 12th EMEA Academic Forum, Intel Corporation, 2200 Mission College Blvd., Santa Clara, CA, USA, June 2007 |
2006 (7)
Refereed (journals/proceedings)
| PDF |
Kofroň J., Adámek J., Bureš T., Ježek P., Mencl V., Parízek P., Plášil F.: Checking Fractal Component Behavior Using Behavior Protocols,
Presented at the 5th Fractal Workshop (part of ECOOP'06), July 3rd, 2006, Nantes, France, July 2006 |
| PDF, Link |
Ježek P., Kofroň J., Plášil F.: Model Checking of Component Behavior Specification: A Real Life Experience,
In Electronic Notes in Theoretical Computer Science, Vol. 160, pp. 197-210, Elsevier B.V., ISSN: 1571-0661, August 2006 |
Technical Reports
| PDF |
Parízek P., Plášil F., Kofroň J.: Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker,
Tech. Report No. 2006/2, Dep. of SW Engineering, Charles University, January 2006 |
| PDF |
Parízek P., Plášil F.: Modeling Environment for Component Model Checking from Hierarchical Architecture,
Published in Preliminary Proceedings of 3rd International Workshop on Formal Aspects of Component Software (FACS'06), Prague, Czech Republic, September 20-22, 2006, UNU-IIST Report No. 344, September 2006 |
Master Theses
| PDF |
Poch T.: Distributed Behavior Protocol Checker,
Master thesis, advisor: Jan Kofron, September 2006 |
| PDF, ZIP, WWW |
Drazan J.: Natural Language Processing of Textual Use Cases,
Master thesis, advisor: Vladimir Mencl, February 2006 |
| PDF |
Šerý O.: Model Checking and Reduction of Behavior Protocols,
Master thesis, advisor: Frantisek Plasil, May 2006 |
2005 (4)
Refereed (journals/proceedings)
| Link |
Adámek J., Plášil F.: Component Composition Errors and Update Atomicity: Static Analysis,
Journal of Software Maintenance and Evolution: Research and Practice 17(5), pp. 363-377, DOI: 10.1002/smr.321, Online ISSN: 1532-0618, Print ISSN: 1532-060X, September 2005
(preliminary version available here)
|
| PDF, Link |
Mencl V., Bureš T.: Microcomponent-Based Component Controllers: A Foundation for Component Aspects,
in Proceedings of 12th Asia-Pacific Software Engineering Conference (APSEC 2005), Dec 15-17, 2005, Taipei, Taiwan, pp. 729-738, ISBN 0-7695-2465-6, ISSN 1530-1362, IEEE Computer Society Press, December 2005 |
Technical Reports
| PDF |
Kofroň J.: Enhancing Behavior Protocols with Atomic Actions,
Tech. Report No. 2005/8, Dep. of SW Engineering, Charles University, Prague, November 2005 |
| PDF |
Parízek P., Plášil F.: Specification and Generation of Environment for Model Checking of Software Components,
Tech. Report No. 2005/5, Dep. of SW Engineering, Charles University, November 2005 |
2004 (3)
Refereed (journals/proceedings)
| PDF |
Mencl V.: Deriving Behavior Specifications from Textual Use Cases,
in Proceedings of Workshop on Intelligent Technologies for Software Engineering (WITSE04, Sep 21, 2004, part of ASE 2004), Linz, Austria, ISBN 3-85403-180-7, pp. 331-341, Oesterreichische Computer Gesellschaft, September 2004 |
Ph.D. Theses
| PDF, PDF |
Mencl V.: Use Cases: Behavior Assembly, Behavior Composition and Reasoning,
Ph.D. Thesis, advisor: Frantisek Plasil, June 2004 |
Technical Reports
| PDF |
Mencl V.: Converting Textual Use Cases into Behavior Specifications,
Tech. Report No. 2004/5, Dept. of SW Engineering, Charles University, Prague, August 2004 |
2003 (2)
Refereed (journals/proceedings)
| PDF |
Plášil F., Mencl V.: Getting "Whole Picture" Behavior in a Use Case Model,
in Proceedings of IDPT 2003, Austin, Texas, U.S.A., ISSN 1090-9389, abstract pp. 23, full paper on CD in session-4/p-4-4.pdf, published by Society for Design and Process Science, Grandview, Texas, awarded with Rudolf Christian Karl Diesel Best Paper Award, also published in Transactions of the SDPS: Journal of Integrated Design and Process Science, vol. 7, no. 4, pp. 63-79, December 2003 |
| PDF |
Plášil F., Mencl V.: Getting "Whole Picture" Behavior in a Use Case Model,
in Transactions of the SDPS: Journal of Integrated Design and Process Science, vol. 7, no. 4, pp. 63-79, Dec 2003, ISSN-1092-0617, publisher: Society for Design and Process Science, Grandview, Texas, slightly modified version of paper published in Proceedings of IDPT 2003, December 2003 |
2002 (1)
Technical Reports
| PDF |
Plášil F., Mencl V.: Use Cases: Assembling "Whole Picture" Behavior,
Technical Report 02/11, Department of Computer Science, University of New Hampshire, NH, U.S.A., November 2002 |
|
Home
People
Research
Projects
Publications
Links
Contact
Teaching
