GRAphische Spezifikation und Echtzeitverifikation von Produktionsautomatisierungssystemen (GRASP)

Publications

2004

• S. Flake, W. Mueller. An ASM Definition of the Dynamic OCL 2.0 Semantics. (accepted for Springer LNCS publication at the UML 2004 Conference, Lisbon, October 2004)
• S. Flake, W. Mueller. Past- and Future-Oriented Temporal Time-Bounded Properties with OCL. (accepted for IEEE publication at the SEFM 2004 Conference, Beijing, China, September 2004)
• S. Flake, W. Mueller, U. Pape, J. Ruf. Specification and Formal Verification of Temporal Properties of Production Automation Systems. In: Final Documenation of the DFG Priority Programme SoftSpec "Integration of Software Specification Techniques for Applications in Engineering", volume 3147 of Lecture Notes in Computer Science, Springer, 2004.
• J. Ruf, T. Kropf, R. Weiss. Modeling and Formal Verification of Production Automation Systems. In: Final Documenation of the DFG Priority Programme SoftSpec "Integration of Software Specification Techniques for Applications in Engineering", volume 3147 of Lecture Notes in Computer Science, Springer, 2004.
• S. Flake. Enhancing the Message Concept of the Object Constraint Language. In 16th International Conference on Software Engineering and Knowledge Engineering (SEKE 2004), Banff, Canada, June 20-24, 2004, pp. 161-166. Knowledge Systems Institute, Skokie, IL, USA.
• P.M. Peranandam, R.J. Weiss, J. Ruf, T. Kropf. Transactional Level Verification and Coverage Metrics by Means of Symbolic Simulation. In D. Stoffel, W. Kunz, editors, 7. GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Kaiserslautern, Germany, February 2004, pp. 260-269. Shaker Verlag, Aachen, Germany, 2004
• S. Flake. Towards the Completion of the Formal Semantics of OCL 2.0. In 27th Conference on Australasian Computer Science (ACSC 2004), Dunedin, New Zealand, January 2004. ACM International Conference Proceeding Series, Australian Computer Science Communications, Volume 26, Number 1, pp. 73 - 82. Australian Computer Science Society, Sydney, Australia, 2004.

2003

• S. Flake. UML-Based Specification of State-Oriented Real-Time Properties. PhD Thesis. Universität Paderborn, Fakultät für Elektrotechnik, Mathematik und Informatik, December 2003. C-LAB Publication, Number 16. Shaker Verlag, Aachen, Germany, 2003.
• S. Flake. Modeling and Verification of Manufacturing Systems: A Domain-Specific Formalization of UML. In 7th IASTED International Conference on Software Engineering and Applications (SEA 2003), Los Angeles, CA, USA, November 2003.
• S. Flake, W. Mueller. Formal Semantics of Static and Temporal State-Oriented OCL Constraints. In Journal on Software and System Modeling (SoSyM), 2(3), pages 164-186, Springer, October 2003.
• H. Giese, M. Tichy, S. Burmester, W. Schaefer, S. Flake. Towards the Compositional Verification of Real-Time UML Designs. In European Software Engineering Conference (ESEC 2003), Helsinki, Finland. September 2003.
• J. Ruf, T. Kropf. Symbolic Verification and Analysis of Discrete Timed Systems. In Journal on Formal Methods in System Design, 23(1): 67-108, July 2003. Kluwer Academic Publishers, 2003.
• S. Flake, W. Mueller. Semantics of State-Oriented Expressions in the Object Constraint Language. In Fifteenth International Conference on Software Engineering and Knowledge Engineering (SEKE 2003), San Francisco, USA. July 2003.
• S. Flake, W. Mueller. Expressing Property Specification Patterns with OCL. In The 2003 International Conference on Software Engineering Research and Practice (SERP'03), Las Vegas, Nevada, USA. June 2003.
• J. Ruf, T. Kropf. Bounded Property Checking with Symbolic Simulation. In Proceedings of GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, February 2003, Bremen, Germany.

2002

• J. Klose, T. Kropf, J. Ruf. A Visual Approach to Validating System Level Designs. In International Symposium on System Level Design (ISSS 2002), Kyoto, Japan, October 2002.
• S. Flake, W. Mueller. A UML Profile for Real-Time Constraints with the OCL. In J.-M. Jezequel, H. Hussmann, S. Cook (eds.), UML 2002 - The Unified Modeling Language, Dresden, Germany, September 30 - October 4, 2002. LNCS 2460, Springer-Verlag, Heidelberg, Germany, September 2002.
• S. Flake. A UML Profile for MFERT. Technical Report, C-LAB Report 04/2002, Paderborn, Germany, June 2002.
• S. Flake. Position Paper on Real-Time Constraints with the OCL. In 5th IEEE International Symposium on Object-oriented Real-time distributed Computing (ISORC2002), Crystal City, VA, USA, April 2002.
• S. Flake, W. Mueller. Temporale Erweiterungen der OCL - Überblick und Aussichten. In 2. Workshop "Ablaufmodellierung in ingenieurwissenschaftlichen Anwendungen", Halle(Saale), Germany, April 2002. (in German)
• J. Ruf, T. Kropf. Verification and Analysis of Discrete Timed Systems. In Journal on Formal Methods in System Design, Kluwer Academic Publishers. (submitted for publication)
• J. Ruf, T. Kropf. Formal Data Analysis of Timed Finite State Systems. In 14th Euromicro Conference on Real-Time Systems (ECRTS), Vienna, Austria, June 2002.
• W. Dangelmaier, C. Darnedde, S. Flake, W. Mueller, U. Pape, H. Zabel. Graphische Spezifikation und Echtzeitverifikation von Produktionsautomatisierungssystemen. In 4. Paderborner Frühlingstagung 2002, ALB-HNI-Verlagsschriftenreihe, Paderborn, Germany, April 2002.
• S. Flake and W. Mueller. An OCL Extension for Real-Time Constraints. In: T. Clark and J. Warmer (eds.), Object Modeling with the OCL, pp. 150-171, LNCS 2263, Springer-Verlag, Heidelberg, February 2002.
• S. Flake and W. Mueller. Specification of Real-Time Properties for UML Models. In Proceedings of the Hawai'i International Conference on System Sciences (HICSS-35), January 2002, Big Island, Hawaii, USA.
• J. Ruf, T. Kropf. Combination of Simulation and Formal Verification. In GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Tübingen, Germany, February 2002.

2001

• S. Flake, W. Mueller. Schnittstellendefinition zur 3D-Animation eines holonischen Fertigungssystems. Technischer Bericht, C-LAB Report 09/2001, Paderborn, Germany, August 2001. (in German)
• J. Quintanilla de Simsek. Ein Verifikationsansatz für eine netzbasierte Modellierungsmethode für Fertigungssysteme. Dissertation, Universität Paderborn, Heinz Nixdorf Institut, HNI-Verlagsschriftenreihe, Band 87, 2001. (in German)
• S. Flake, C. Geiger, W. Mueller, V. Paelke, W. Rosenbach, and J. Ruf. Customer-Oriented Systems Design through Virtual Prototypes, In Proceedings of IEEE 10th Int. Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises (WET ICE'01), Cambridge, MA, USA, June 2001.
• J. Ruf, D.W. Hoffmann, T. Kropf, and W. Rosenstiel. Simulation-Guided Property Checking Based on Multi-Valued AR-Automata. In Proceedings of Design Automation and Test in Europe (DATE), Munich, March 2001, IEEE Computer Society Press, Los Alamitos.
• S. Flake, W. Mueller, U. Pape, and J. Ruf. Analyzing Timing Constraints in Flexible Manufacturing Systems. In Proceedings of Intelligent Manufacturing Systems (IAM'2001). Dubai, March 2001.
• J. Ruf. RAVEN: Real-Time Analyzing and Verification Environment. In Journal on Universal Computer Science (J.UCS), February 2001, Springer-Verlag, Heidelberg.
• W. Reif, J. Ruf, G. Schellhorn, and T. Vollmer. Correctness of Efficient Real-Time Model Checking. In Journal on Universal Computer Science (J.UCS), February 2001, Springer-Verlag, Heidelberg.
• J. Ruf. Data Analysis of Timed Finite State Systems. In Proceedings of GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Meissen, Germany, February 2001.
• J. Ruf, T. Kropf. Formale Verifikation diskreter Echtzeitsysteme. In it+ti Informationstechnik und technische Informatik, Oldenbourg Verlag, Munich, Germany, February 2001.

2000

• J. Ruf, D. Hoffmann, T. Kropf, and W. Rosenstiel. Checking Temporal Properties under Simulation of Executable Specifications. In Proceedings of Workshop on High Level Descriptions and Verification Techniques (HLDVT 2000), Stanford, CA, November 2000, IEEE Computer Society Press.
• W. Reif, J. Ruf, G. Schellhorn, and T. Vollmer. Do You Trust Your Model Checker? In Proceedings of Formal Methods in Computer Aided Design (FMCAD 2000), Austin, Texas, November 2000, Springer-Verlag, Heidelberg.
• S. Flake, W. Mueller, U. Pape, and J. Ruf. Modellprüfung für den Entwurf von Fertigungssteuerungssystemen. In GI-Fachtagung "Modellierung betrieblicher Informationssysteme" (MobIS 2000), Siegen, Germany, October 2000. (in German)
• P.C.P. Bhatt, W. Mueller. A Methodology for the Protocol-Centered Design of Agent-Based Systems. IECON 2000, Nagoya, Japan, October 2000.
• J. Ruf, D. Hoffmann, T. Kropf and W. Rosenstiel. Simulation Based Validation of FLTL Formulas in Executable System Descriptions. In Proceedings of Forum on Design Languages (FDL 2000), Tübingen, Germany, September 2000.
• P.C.P. Bhatt, W.Mueller. Morphic Nets: Model Based Design Diagrams. In UKPEW 2000, Durham, UK, June 2000.
• S. Flake and C. Geiger. Agents with Complex Plans: Design and Implementation of CASA. In 2nd International Symposium "From Agent Theory to Agent Implementation", EMCSR 2000, Vienna, Austria, April 2000.
• J. Ruf and T. Kropf. Analyzing Real-Time Systems. In Design, Automation and Test in Europe (DATE), Paris, France, March 2000, IEEE Computer Society Press.
• J. Ruf. Techniken zur Modellierung und Verifikation von Echtzeitsystemen. Dissertation, Universität Karlsruhe, Logosverlag Berlin, March 2000.
• A. Braatz, S. Flake, W. Mueller, and E. Westkaemper. Prototyping einer Fahrzeugsteuerung in virtueller 3D-Umgebung. In Simulation und Visualisierung 2000, Magdeburg, Germany, March 2000. (in German)
• S. Flake, W. Mueller, and J. Ruf. Structured English for Model Checking Specification. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, GI/ITG/GMM Workshop, Frankfurt/M., Germany, February 2000.
• J. Ruf. A Toolest for the Symbolic Examination of Finite State Transition Systems. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, GI/ITG/GMM Workshop, Frankfurt/M., Germany, February 2000.
• J. Ruf. Verification of Timing Properties of a Holonic Manufacturing System. Technical Report WSI-2000-03, Universität Tübingen, February 2000.
• J. Ruf. RAVEN: Real-Time Analyzing and Verification Environment. Technical Report WSI-2000-02, Universität Tübingen, February 2000.
• S. Flake, W. Mueller, and J. Ruf. An Advanced Visual Capture for Model Checking Specifications. Technical Report, C-LAB Report 05/2000, Paderborn, Germany, February 2000.
• S. Flake, W. Mueller, and J. Ruf. Mapping of Structured English Sentences to CCTL Formulae. Technical Report, C-LAB Report 04/2000, Paderborn, Germany, January 2000.

1999

• S. Flake and C. Geiger. CASA - Structured Design of a Specification Language for Intelligent Agents. In 5th Asian Computing Science Conference (ASIAN'99), Phuket, Thailand, December 1999. Springer Verlag Heidelberg, LNCS 1742.
• J. Ruf and T. Kropf. Modeling and Checking Netwerks of Communicating Real-Time Processes. In Conference on Correct Hardware Design and Verification Methods (CHARME), pp. 265-279, Bad Herrenalb, Germany, October 1999. IFIP WG 10.5, Springer Verlag, LNCS 1703.
• S. Flake, C. Geiger, G. Lehrenfeld, W. Mueller, and V. Paelke. Agent-Based Modeling for Holonic Manufacturing Systems with Fuzzy Control. 18th International Conference of the North American Fuzzy Information Processing Society (NAFIPS'99), New York, USA, June 1999.
• S. Flake Entwurf und prototypische Realisierung einer Spezifikationssprache für intelligente Software-Agenten Diploma Thesis, Universität Paderborn, Germany, May 1999. (in German)
• J. Ruf and T. Kropf. Modeling Real-Time Systems with I/O-Interval Structures. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pp. 91-100. GI/ITG/GMM Workshop, Braunschweig, Germany, Shaker Verlag, March 1999.

1998

• J. Ruf and T. Kropf. Using MTBDDs for Composition and Model Checking of Real-Time Systems. In Formal Methods in Computer Aided design (FMCAD), Palo Alto, CA, November 1998. Springer-Verlag, November 1998.