photo of Jan Kubovy
 

Publications

2014

  1. Kubovy J., Küng J.: Embedding formal models into Latex documents, in Journal of Science and Technology VAST Vietnam, Special Issue on International Conference on Advanced Computing and Applications, ACOMP 2014, Journal of Science and Technology, Vol. 52, Nummer 4A, Seite(n) 83-90, 11-2014. BibTeX pdf

    Formal methods proved themselves to support provable and unambiguous models. Still a lot of manual work is needed to assure consistency during the modeling process. In this paper we propose a support tool in form of a latex package helping a modeler to embed formal code and related description into a specification document. This package helps to assure relative consistency between abstraction levels, structuring the formal ground model, and improving the reuse of parts of the ground model in different stages of the specification cycle.

  2. Kubovy J.: Behavior approached decomposition of the BPMN 2.0 with enhanced refinements preserving the semantics of the ground model, 2014. BibTeX pdf

    This thesis shows a decomposition of the Business Process Model and Notation (BPMN) meta-model based on behaviors. The different BPMN flow node types are then composed using these behaviors defined in the BPMN 2.0 standard. Composition of the different flow node types using these behavior patterns is demonstrated with modifications of the BPMN meta-model hierarchy to improve the target Abstract State Machine (ASM) ground model.

    A formal specification of the control flow in a BPMN Workflow Engine (WFE) is then introduced using the ASM method. We call the part of BPMN WFE, which is responsible only for the control flow of a BPMN process the Workflow Interpreter (WFI). The ASM method allows describing a system formally on a certain abstraction level. However this abstraction level can change during the process of designing a system as a result of refinements. The way a system needs to be described on an abstract level usually differs from the way a system is described when more concrete specifics are known. In this thesis we introduce two basic abstraction levels, their semantics, show how to realize transition of the related documents describing the system from one abstraction level to another and how to preserve consistency of the specification documents between both levels in case of changes. An example is made on the BPMN specification, which is first described on a business level and further transits to a technical level.

    Targeting the WFI, focus is also put on simplification and reusability im provement of the resulting implementation contributing to meta-model hierarchy change. Furthermore, the BPMN non-trivial activation concept, event flow and some other parts of the BPMN specification are refined. One of core refinement is the concrete formal definition of upstream token concept and calculation of the enableness of an inclusive gateways. The introduced algorithm for upstream token calculation considers also situations where two or more gateways are mutually dependent. Another is clarification and clear separation of events, timer triggers and notifications, definition of message and signal pools, and formal definition of the different event forwarding concepts.

  3. Kubovy J., Auer D., Küng J., Rady M.: Transition between different abstraction levels in an Abstract State Machine (ASM) ground model, in: Database and Expert Systems Applications (DEXA), 2013 24th International Workshop on, Series Database and Expert Systems Applications (DEXA), Page(s) 227-230, IEEE, 2013. BibTeX pdf

    Using Abstract State Machines (ASMs) we can specify a service or piece of software formally for the purpose of future implementation. During the development life-cycle the related specification evolves. Abstract functions and rules are defined, new functions and rules are introduced and arbitrary data structures are instantiated with the specification being refined towards implementation. Two main abstraction levels are introduced in this paper to show a possible classification of abstraction levels of a formal specification. Furthermore, the basic differences and basic transition guidelines between those levels are discussed. A small example of the proposed two main abstraction levels is shown on a high-level specification of a potential transition machine to outline the intended transition process, typical appearance of abstraction level stages and refinement patterns.

  4. Kossak F., Illibauer C., Geist V., Kubovy J., Natschläger C., Ziebermayr T., Kopetzky T., Freudenthaler B., Schewe K.: A Rigorous Semantics for BPMN 2.0 Process Diagrams, Springer, 233 page(s), 2014. BibTeX

    This book provides the most complete formal specification of the semantics of the Business Process Model and Notation 2.0 standard (BPMN) available to date, in a style that is easily understandable for a wide range of readers – not only for experts in formal methods, but e.g. also for developers of modeling tools, software architects, or graduate students specializing in business process management.

  5. Kubovy J., Küng J.: Renement of BPMN 2.0 Inclusive and Complex Gateway Activation Concept towards Process Engine, in: Novel Methods and Technologies for Enterprise Information Systems, Series LNISO, Volume 8, Page(s) 55-62, Springer International Publishing, 2014. BibTeX pdf

    This paper presents a possible refinement of Business Process Model and Notation (BPMN) Gateway activation concept for non-event-based gateways. The core refinement is the concrete formal definition of upstream token concept and calculation of the enabledness of an inclusive gateways (or also Or-Join) using modified Dijkstra’s algorithm. The introduced algorithm for upstream token calculation considers also situations where two or more gateways are mutually dependent.

  6. Kubovy J., Auer D., Küng J., "Behavior-based Decomposition of BPMN 2.0 Control Flow" : 16th International Conference on Enterprise Information Systems, Pages 263--271, 2014 BibTeX pdf

    The Business Process Model and Notation (BPMN) is a well-established industry standard in the area of Business Process Management (BPM). However, still with the current version 2.0 of BPMN, problems and contradictions with the underlying semantics of the meta-model can be identified. This paper shows an alternative approach for modeling the BPMN meta-model, using behavior-based decomposition. The focus in this paper is on control flow. We use Abstract State Machines (ASM) to describe the decomposition of the merging and splitting behavior of the different BPMN flow node types, such as parallel, exclusive, inclusive and complex, as defined in the BPMN 2.0 standard, resulting in behavior patterns. Furthermore an example for the composition of different gateway types is given using these behavior patterns.

2013

  1. Auer D., Hinterholzer S., Kubovy J., Küng J.: Business Process Management for Knowledge Work: Considerations on Current Needs, Basic Concepts and Models, in: Piazolo, Felix and Felderer, Michael (Eds.): Novel Methods and Technologies for Enterprise Information Systems, Series Lecture Notes in Information Systems and Organisation, Volume 8, Page(s) 79-95, Springer International Publishing, 2014. BibTeX

    The portion of knowledge work is steadily increasing in todays working environments in western societies. This needs to be respected in the supporting IT systems. Starting with the characteristics of knowledge work and the resulting needs of knowledge workers, we present and compare two current standardization efforts in area of Business Process Management (BPM) by the OMG?the Business Process Model and Notation (BPMN) and the Case Management Model and Notation (CMMN). We argue that a hybrid approach will not suffice in the future, but that there is rather a strong need for full integration.

  2. Kubovy J., Küng J.: Notification Concept for BPMN Workflow Interpreter Using the ASM Method, in: Computer Aided Systems Theory- EUROCAST 2013, Series Lecture Notes in Computer Science, Page(s) 452-459, Springer, 2013. BibTeX pdf

    In this paper we focus on filling the gap between the formal Business Process Model and Notation (BPMN) Abstract State Machine (ASM) ground model and a Workflow Interpreter (WI) implementation. For that purpose we use an execution context concept and notification concept, a refinement of triggers (event definitions).

  3. Kubovy J., Rady M., Auer D., Küng J.: Abstraction levels in the Abstract State Machine (ASM) method for system specification, in: Journal of Science and Techology - Special Issue on International Conference on Advanced Computing and Applications, ACOMP 2013, Series Journal of Science and Technology, Volume 51, Number 4B, Page(s) 1-9, Vietnam Academy of Science and Techology, 2013. BibTeX pdf

    The ASM method allows describing a system formally on a certain abstraction level [see 1–3; 8]. However this abstraction level can change during the process of designing a system as a result of refinements. The way a system needs to be described on an abstract level usually differs from the way a system is described when more concrete specifics are known. In this paper we introduce two basic abstraction levels, their semantics, show how to realize transition from one abstraction level to another and how to preserve consistency in both levels in case of changes.

2012

  1. Kubovy, J.; Geist, V.; Kossak, F., "A Formal Description of the ITIL Change Management Process Using Abstract State Machines," in Database and Expert Systems Applications (DEXA), 2012 23rd International Workshop, pp.65-69, 3-7 Sept. 2012. BibTeX pdf

    We suggest formalising Information Technology Infrastructure Library (ITIL) processes using the Business Process Model and Notation (BPMN) and the Abstract State Machine (ASM) method. We describe the benefits of our approach as well as the necessary prerequisites. We argue that such a formalisation will lead to a clearer understanding of the process and a reduction of ambiguity.

2011

  1. Kubovy J.: Network Media Content Aggregator for DLNA Server, 2011. BibTeX pdf

    This thesis engages in solving problem of collecting media files from different sources in the network, identify them, sort them and make them available to other devices in the network. Identification and removal of duplicates and gathering additional information such as author, album, date, etc. This thesis is divided into two parts. In the first part a technology and market overview of existing devices, software and similar solutions can be found. The second part introduces one solution and shows the implementation of such solution. Further possibilities of the implementation will be also discussed.

2010

  1. Št'astný, J.; Doležal, J.; Černý, V.; Kubovy, J., "Design of a modular brain-computer interface," in Applied Electronics (AE), 2010 International Conference on , vol., no., pp.1-4, 8-9 Sept. 2010. BibTeX pdf

    We have been dealing with a research in the field of movement-related EEG recognition and currently we are working on an off-line single trial classification system able to recognize movement-related EEG on the base of its temporal development. This contribution presents a preliminary study of the proposed real-time BCI system architectural components for the EEG Processing Pipeline along with the results of the design of the first fundamental system blocks. The project also successfully involves students of our department in a real teamwork.

2005- © Me