Högskolan i Skövde

his.sePublications
Change search
Link to record
Permanent link

Direct link
Ericsson, AnnMarie
Alternative names
Publications (10 of 12) Show all publications
Ericsson, A., Berndtsson, M. & Mellin, J. (2009). Active Database Rulebase. In: Ling Liu, M. Tamer Özsu (Ed.), Encyclopedia of Database Systems: (pp. 37-37). Springer Science+Business Media B.V.
Open this publication in new window or tab >>Active Database Rulebase
2009 (English)In: Encyclopedia of Database Systems / [ed] Ling Liu, M. Tamer Özsu, Springer Science+Business Media B.V., 2009, p. 37-37Chapter in book (Other academic)
Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2009
National Category
Computer and Information Sciences
Research subject
Technology
Identifiers
urn:nbn:se:his:diva-7046 (URN)10.1007/978-0-387-39940-9_510 (DOI)978-0-387-49616-0 (ISBN)978-0-387-35544-3 (ISBN)978-0-387-39940-9 (ISBN)
Available from: 2013-02-06 Created: 2013-01-24 Last updated: 2023-06-16Bibliographically approved
Ericsson, A., Berndtsson, M. & Mellin, J. (2009). Composite Event. In: Ling Liu, M. Tamer Özsu (Ed.), Encyclopedia of Database Systems: (pp. 418-419). Springer Science+Business Media B.V.
Open this publication in new window or tab >>Composite Event
2009 (English)In: Encyclopedia of Database Systems / [ed] Ling Liu, M. Tamer Özsu, Springer Science+Business Media B.V., 2009, p. 418-419Chapter in book (Other academic)
Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2009
National Category
Computer and Information Sciences
Research subject
Technology
Identifiers
urn:nbn:se:his:diva-7059 (URN)10.1007/978-0-387-39940-9_514 (DOI)978-0-387-49616-0 (ISBN)978-0-387-35544-3 (ISBN)978-0-387-39940-9 (ISBN)
Available from: 2013-02-06 Created: 2013-01-28 Last updated: 2023-06-16Bibliographically approved
Ericsson, A. (2009). Enabling Tool Support for Formal Analysis of ECA RUles. (Doctoral dissertation). Linköpings universitet
Open this publication in new window or tab >>Enabling Tool Support for Formal Analysis of ECA RUles
2009 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Rule-based systems implemented as event-condition-action (ECA) rules utilize a powerful and flexible paradigm when it comes to specifying systems that need to react to complex situation in their environment. Rules can be specified to react to combinations of events occurring at any time in any order. However, the behavior of a rule based system is notoriously hard to analyze due to the rules ability to interact with each other.

Formal methods are not utilized in their full potential for enhancing software quality in practice. We argue that seamless support in a high-level paradigm specific tool is a viable way to provide industrial system designers with powerful verification techniques. This thesis targets the issue of formally verifying that a set of specified rules behaves as indented.

The prototype tool REX (Rule and Event eXplorer) is developed as a proof of concept of the results of this thesis. Rules and events are specified in REX which is acting as a rule-based front-end to the existing timed automata CASE tool UPPAAL. The rules, events and requirements of application design are specified in REX. To support formal verification, REX automatically transforms the specified rules to timed automata, queries the requirement properties in the model-checker provided by UPPAAL and returns results to the user of REX in terms of rules and events.

The results of this thesis consist of guidelines for modeling and verifying rules in a timed automata model-checker and experiences from using and building a tool implementing the proposed guidelines. Moreover, the result of an industrial case study is presented, validating the ability to model and verify a system of industrial complexity using the proposed approach.

Place, publisher, year, edition, pages
Linköpings universitet, 2009. p. 150
Series
Linköping Studies in Science and Technology, Dissertations,, ISSN 0345-7524 ; 1262
Keywords
ECA rules, Timed automata, Formal verification
National Category
Engineering and Technology
Research subject
Technology
Identifiers
urn:nbn:se:his:diva-3206 (URN)978-91-7393-598-2 (ISBN)
Public defence
(English)
Available from: 2009-06-26 Created: 2009-06-26 Last updated: 2017-11-27Bibliographically approved
Ericsson, A., Berndtsson, M. & Mellin, J. (2009). Event in Active Databases. In: Ling Liu, M. Tamer Özsu (Ed.), Encyclopedia of Database Systems: (pp. 1044-1045). Springer Science+Business Media B.V.
Open this publication in new window or tab >>Event in Active Databases
2009 (English)In: Encyclopedia of Database Systems / [ed] Ling Liu, M. Tamer Özsu, Springer Science+Business Media B.V., 2009, p. 1044-1045Chapter in book (Other academic)
Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2009
National Category
Computer and Information Sciences
Research subject
Technology
Identifiers
urn:nbn:se:his:diva-7069 (URN)10.1007/978-0-387-39940-9_512 (DOI)978-0-387-49616-0 (ISBN)978-0-387-35544-3 (ISBN)978-0-387-39940-9 (ISBN)
Available from: 2013-02-06 Created: 2013-01-28 Last updated: 2023-06-16Bibliographically approved
Ericsson, A., Berndtsson, M., Pettersson, P. & Pettersson, L. (2008). Verification of an industrial rule-based manufacturing system using REX. In: Darko Anicic, Christian Brelage, Opher Etzion, Nenad Stojanovic (Ed.), Proceedings of the 1st iCEP08 Workshop onComplex Event Processing for the Future Internet Vienna, Austria, September 28th, 2008: . Paper presented at The 1st International workshop on Complex Event Processing for the Future Internet - Realizing Reactive Future Internet, FIS 2008, Vienna, Austria, September 28th, 2008 (pp. 1-10). CEUR-WS.org, Article ID 2.
Open this publication in new window or tab >>Verification of an industrial rule-based manufacturing system using REX
2008 (English)In: Proceedings of the 1st iCEP08 Workshop onComplex Event Processing for the Future Internet Vienna, Austria, September 28th, 2008 / [ed] Darko Anicic, Christian Brelage, Opher Etzion, Nenad Stojanovic, CEUR-WS.org , 2008, p. 1-10, article id 2Conference paper, Published paper (Refereed)
Abstract [en]

Formal methods are not used in their full potential for enhancing software quality in industry. We argue that seamless support in a high-level specification tool is a viable way to provide system designers with powerful and paradigm specific formal verification techniques. Event condition action (ECA) rules can be used to model and implement reactive behavior in, for example, the semantic web. Independently of target system, the behavior of rule-based systems are known to be hard to analyze. The REX tool is a rule-based front-end to the timed automata CASE-tool Uppaal. The model-checker in Uppaal is used by REX enabling seamless support for model-checking rule-based specifications in REX.

This paper presents experiences from modeling and verifying a system of industrial complexity as interacting rules using EX. We conclude that repeatedly performing normal analysis when constructing a system with interacting rules is a viable way of coping with the complexity of the model. Additionally, we present an implemented algorithm for optimizing the model to reduce the effect of state-space explosion.

Place, publisher, year, edition, pages
CEUR-WS.org, 2008
Series
CEUR WS series, ISSN 1613-0073 ; 412
National Category
Computer and Information Sciences
Research subject
Technology
Identifiers
urn:nbn:se:his:diva-2573 (URN)2-s2.0-84885604285 (Scopus ID)
Conference
The 1st International workshop on Complex Event Processing for the Future Internet - Realizing Reactive Future Internet, FIS 2008, Vienna, Austria, September 28th, 2008
Available from: 2009-01-21 Created: 2009-01-21 Last updated: 2023-06-16Bibliographically approved
Ericsson, A. (2008). Verifying an industrial system using REX. Skövde: Institutionen för kommunikation och information
Open this publication in new window or tab >>Verifying an industrial system using REX
2008 (English)Report (Other academic)
Abstract [sv]

Användandet av formella metoder för att höja kvalitén på mjukvara används inte i någon stor utsträckning inom industrin. Vi hävdar att användandet av ett verktyg där man kan specificera sitt system i ett högnivåspråk istället för direkt i det formella språket är en möjlig väg för att förse mjukvaruutvecklare med kraftfulla verifieringsverktyg som är specifika för olika paradigmer. Verktyget REX stödjer specifikation av applikationer specificerade som en mängd regler och sammansatta händelser. Dessutom tillhandahåller REX stöd för att överföra regelbaserade modeller och applikations specifika krav från REX till det formella verktyget Uppaal. Model-checkern i Uppaal kontrolleras automatiskt av REX. I denna rapport presenteras en fallstudie där ett system som används för att planera produktionen på Volvo IT i Skövde har specificerats som regler och verifierats formellt med hjälp av REX. Syftet med fallstudien är att visa att REX kan användas för att specificera och verifiera ett komplext system som används i verkligheten.

Abstract [en]

The use of formal methods for enhancing software quality is still not used in its full potential in industry. We argue that seamless support in a high-level specification tool is a viable way to provide industrial system designers with complex and powerful formal verification techniques.

The REX tool supports specification of applications constructed as a set of rules and complex events. REX provides seamless support for specifying and verifying application specific requirement properties in the timed automata model-checking tool Uppaal. The rules, events and requirements of an application design is automatically transformed to a timed automaton representation and verified in the Uppaal tool.

In order to validate the applicability of our approach, we present experimental results from a case-study of an industrial system. Based on the case-study results, we conclude that complex applications can be efficiently verified using our approach.

Place, publisher, year, edition, pages
Skövde: Institutionen för kommunikation och information, 2008. p. 45
Series
IKI Technical Reports ; HS-IKI-TR-08-001
National Category
Computer Sciences
Identifiers
urn:nbn:se:his:diva-1284 (URN)
Available from: 2008-06-17 Created: 2008-06-17 Last updated: 2018-01-13
Ericsson, A. & Berndtsson, M. (2007). REX, the Rule and Event eXplorer. In: DEBS '07: Proceedings of the 2007 inaugural international conference on Distributed event-based systems. Paper presented at The 2007 inaugural international conference on Distributed event-based systems, Toronto, June 20 - 22, 2007 (pp. 71-74). New York: Association for Computing Machinery (ACM)
Open this publication in new window or tab >>REX, the Rule and Event eXplorer
2007 (English)In: DEBS '07: Proceedings of the 2007 inaugural international conference on Distributed event-based systems, New York: Association for Computing Machinery (ACM), 2007, p. 71-74Conference paper, Published paper (Refereed)
Abstract [en]

Complex Event Processing (CEP) is a technology with support for matching patterns in a cloud or streams of events in order to support detection of specific combinations of event occurrences. A clever specification of event patterns may, for example, detect fraud attempts in a banking system, fire an alarm in response to hazardous situations in a control system or report suspicious customer behavior.

Several CEP engines have support for graphically modelling applications as well as perform tests and provide execution traces to verify the application behavior. We argue that it is beneficial to complement testing with formal verification in order to detect errors in early stages of development.

In this paper, we present the research prototype tool REX. REX is built as a loosely coupled front end to the timed-automata CASE tool UPPAAL. CEP applications and application specific properties can be specified in REX. To support formal verification, REX seamlessly transforms the CEP application together with the specified properties to the timed automata CASE tool UPPAAL where the properties are verified by the model-checker provided by UPPAAL.

Place, publisher, year, edition, pages
New York: Association for Computing Machinery (ACM), 2007
Series
ACM International Conference Proceeding Series ; 233
Keywords
Design, Verification, CEP, Timed automata
National Category
Computer and Information Sciences
Research subject
Technology
Identifiers
urn:nbn:se:his:diva-2110 (URN)10.1145/1266894.1266906 (DOI)2-s2.0-34548019026 (Scopus ID)978-1-59593-665-3 (ISBN)
Conference
The 2007 inaugural international conference on Distributed event-based systems, Toronto, June 20 - 22, 2007
Note

Copyright © 2007 ACM

Available from: 2008-05-30 Created: 2008-05-30 Last updated: 2021-02-22Bibliographically approved
Ericsson, A., Pettersson, P., Berndtsson, M. & Seirio, M. (2007). Seamless Formal Verification of Complex Event Processing Applications. In: DEBS '07: Proceedings of the 2007 inaugural international conference on Distributed event-based systems. Paper presented at The 2007 inaugural international conference on Distributed event-based systems, Toronto, June 20 - 22, 2007 (pp. 50-61). New York: Association for Computing Machinery (ACM)
Open this publication in new window or tab >>Seamless Formal Verification of Complex Event Processing Applications
2007 (English)In: DEBS '07: Proceedings of the 2007 inaugural international conference on Distributed event-based systems, New York: Association for Computing Machinery (ACM), 2007, p. 50-61Conference paper, Published paper (Refereed)
Abstract [en]

Despite proven successful in previous projects, the use of formal methods for enhancing quality of software is still not used in its full potential in industry. We argue that seamless support for formal verification in a high-level specification tool enhances the attractiveness of using a formal approach for increasing software quality.

Commercial Complex Event Processing (CEP) engines often have support for modelling, debugging and testing CEP applications. However, the possibility of utilizing formal analysis is not considered.

We argue that using a formal approach for verifying a CEP system can be performed without expertise in formal methods. In this paper, a prototype tool REX is presented with support for specifying both CEP systems and correctness properties of the same application in a high-level graphical language. The specified CEP applications are seamlessly transformed into a timed automata representation together with the high-level properties for automatic verification in the model-checker UPPAAL.

Place, publisher, year, edition, pages
New York: Association for Computing Machinery (ACM), 2007
Series
ACM International Conference Proceeding Series ; 233
Keywords
Design, Verification, CEP, Timed automata
National Category
Computer and Information Sciences
Research subject
Technology
Identifiers
urn:nbn:se:his:diva-2111 (URN)10.1145/1266894.1266903 (DOI)2-s2.0-34548032816 (Scopus ID)978-1-59593-665-3 (ISBN)
Conference
The 2007 inaugural international conference on Distributed event-based systems, Toronto, June 20 - 22, 2007
Note

Copyright © 2007 ACM

Available from: 2008-05-30 Created: 2008-05-30 Last updated: 2021-02-22Bibliographically approved
Lindström, B., Nilsson, R., Ericsson, A., Grindal, M., Andler, S. F., Eftring, B. & Offutt, J. (2007). Six Issues in Testing Event-Triggered Real-Time Systems. Skövde: Institutionen för kommunikation och information
Open this publication in new window or tab >>Six Issues in Testing Event-Triggered Real-Time Systems
Show others...
2007 (English)Report (Other academic)
Abstract [en]

Verification of real-time systems is a complex task, with problems coming from issues like concurrency. A previous paper suggested dealing with these problems by using a time-triggered design, which gives good support both for testing and formal analysis. However, a

time-triggered solution is not always feasible and an event-triggered design is needed. Event-triggered systems are far more difficult to test than time-triggered systems.

This paper revisits previously identified testing problems from a new perspective and identifies additional problems for event-triggered systems. The paper also presents an approach to deal with these problems. The TETReS project assumes a model-driven development

process. We combine research within three different fields: (i) transformation of rule sets between timed automata specifications and ECA rules with maintained semantics, (ii) increasing testability in event-triggered system, and (iii) development of test case generation methods for event-triggered systems.

Place, publisher, year, edition, pages
Skövde: Institutionen för kommunikation och information, 2007. p. 10
Series
IKI Technical Reports ; HS-IKI-TR-07-005
National Category
Information Systems
Identifiers
urn:nbn:se:his:diva-1269 (URN)
Available from: 2008-06-17 Created: 2008-06-17 Last updated: 2018-09-07Bibliographically approved
Ericsson, A. & Berndtsson, M. (2006). Detecting Design Errors in Composite Events for Event Triggered Real-Time Systems Using Timed Automata. In: Malu Castellanos, Jian Yang (Ed.), SCW 2006: IEEE Services Computing Workshops: 18-22 September 2006, Chicago, Illinois: Proceedings. Paper presented at First International Workshop on Event-driven Architecture, Processing and Systems (EDA-PS 06), IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, Illinois (pp. 39-47). IEEE
Open this publication in new window or tab >>Detecting Design Errors in Composite Events for Event Triggered Real-Time Systems Using Timed Automata
2006 (English)In: SCW 2006: IEEE Services Computing Workshops: 18-22 September 2006, Chicago, Illinois: Proceedings / [ed] Malu Castellanos, Jian Yang, IEEE, 2006, p. 39-47Conference paper, Published paper (Refereed)
Abstract [en]

Many applications need to detect and respond to occurring events and combine these event occurrences into new events with a higher level of abstraction. Specifying how events can be combined is often supported by design tools specific to the current event processing engine. However, the issue of ensuring that the combinations of events provide the system with the correct combination of information is often left to the developer to analyze. We argue that analyzing correctness of event composition is a complex task that needs tool support. In this paper we present a novel development tool for specifying composition of events with time constraints. One key feature of our tool is to automatically transform composite events for real-time systems into a timed automaton representation. The timed automaton representation allow us to check for design errors, for example, whether the outcome of combining events with different operators in different consumption policies is consistent with the requirement specification

Place, publisher, year, edition, pages
IEEE, 2006
National Category
Computer and Information Sciences Computer Sciences Computer Systems
Research subject
Technology; Software Systems Research Group (SSRG)
Identifiers
urn:nbn:se:his:diva-1948 (URN)10.1109/SCW.2006.11 (DOI)000241634600005 ()2-s2.0-35148858794 (Scopus ID)0-7695-2681-0 (ISBN)978-0-7695-2681-2 (ISBN)
Conference
First International Workshop on Event-driven Architecture, Processing and Systems (EDA-PS 06), IEEE Services Computing Workshops (SCW 2006), 18-22 September 2006, Chicago, Illinois
Available from: 2008-04-09 Created: 2008-04-09 Last updated: 2021-03-17Bibliographically approved
Organisations

Search in DiVA

Show all publications