Thiagarajan P.S.,National University of Singapore |
Yang S.,UNU IIST
HSCC'10 - Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control | Year: 2010
We consider a network of hybrid automata that observe and control a plant whose state space is determined by a finite set of continuous variables. We assume that at any instant, these variables are evolving at (possibly different) constant rates. Each automaton in the network controls-i.e. can switch the rates of-a designated subset of the continuous variables without having to reset their values. These mode changes are determined by the current values of a designated subset of the variables that the automaton can observe. We require the variables controlled-in terms of effecting mode changes - by different hybrid automata to be disjoint. However, the same variable may be observed by more than one automaton. We study the discrete time behavior of such networks of hybrid automata. We show that the set of global control state sequences displayed by the network is regular. More importantly, we show that one can effectively and succinctly represent this regular language as a product of local finite state automata. © 2010 ACM.
Liu Z.,UNU IIST |
Roychoudhury A.,National University of Singapore
International Journal on Software Tools for Technology Transfer | Year: 2012
Large scale software engineering is undergoing substantial shifts due to a combination of technological and economic developments. These include the prevalence of software for embedded systems, global software development across geographically distributed teams, the technological shift towards multi-core platforms, and the inevitable shift towards software being used as a service. In this overview article, we discuss some of the challenges that lie ahead for software validation, due to such technological developments. In particular, we provide a brief introduction to the papers appearing in this special issue, many of which specifically focus on validation of software running on real-time embedded systems. © 2012 Springer-Verlag.
Bertolini C.,Federal University of Pernambuco |
Liu Z.,UNU IIST |
Srba J.,University of Aalborg
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2013
Workflows in modern healthcare systems are becoming increasingly complex and their execution involves concurrency and sharing of resources. The definition, analysis and management of collaborative healthcare workflows requires abstract model notations with a precisely defined semantics and a support for compositional reasoning. We use the formalism of component-based timed-arc Petri Nets (CTAPN) for modular modelling of collaborative healthcare workflows and demonstrate how the model checker TAPAAL supports the verification of their functional and non-functional requirements. To this end, we use CTAPN to define the semantics of the healthcare domain specific graphical notation Little-JIL, extended with timing constrains, and apply it to the case study of blood transfusion. The value added in general, and to Little-JIL in particular, is the formal support for modelling, analysis and verification with the explicit treatment of the timing aspects. © 2013 Springer-Verlag.
Li D.,University of Macau |
Li X.,Macau University of Science and Technology |
Liu Z.,UNU IIST |
Stolz V.,University of Oslo
Proceedings of the Australian Software Engineering Conference, ASWEC | Year: 2013
Integrating formal methods into UML opens up a way to complement UML-based software development with precise semantics, development methodologies, as well as rigorous verification and refinement techniques. In this paper, we present an approach to integrate a formal method to practical component-based model driven development through defining a UML profile that maps the concepts of the formal method as UML stereotypes, and implementing the profile into a CASE tool. Unlike most of the previous works in this vein, which concentrate on verifying the correctness of the models built in the development process, we focus on how the full development process can be driven by applying the refinement rules of the formal method in an incremental and interactive manner. The formal method we adopt in this work is the refinement for Component and Object Systems (rCOS). We demonstrate the development activities in the CASE tool using an example. © 2013 IEEE.
Chen Y.,Peking University |
Sanders J.W.,UNU IIST
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2010
A set-theoretic formalism, AOG, is introduced to support automated verification of pointer programs. AOG targets pointer reasoning for source programs before compilation (before removal of field names). Pointer structures are represented as object graphs instead of heaps. Each property in AOG is a relation between object graphs and name assignments of program variables, and specifications result from composing properties. AOG extends Separation Logic's compositions of address-disjoint separating conjunction to more restrictive compositions with different disjointness conditions; the extension is shown to be strict when fixpoints are present. A composition that is a 'unique decomposition' decomposes any given graph uniquely into two parts. An example is the separation between the non-garbage and garbage parts of memory. Although AOG is in general undecidable, it is used to define the semantics of specialised decidable logics that support automated program verification of specific topologies of pointer structure. One logic studied in this paper describes pointer variables located on multiple parallel linked lists. That logic contains quantifiers and fixpoints but is nonetheless decidable. It is applied to the example of in-place list reversal for automated verification, and in outline to the Schorr-Waite marking algorithm. The technique of unique decomposition is found to be particularly useful in establishing laws for such logics. © 2010 Springer-Verlag Berlin Heidelberg.
Bertolini C.,UNU IIST |
Schaf M.,UNU IIST |
Stolz V.,University of Oslo
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2012
Health information systems (HIS) are becoming increasingly integrated through network communication technologies. Collaborative healthcare workflows (CHWF) are inherently complex, involving interactions among human actors, and (legacy) digital and physical systems. They are mission safety critical, privacy sensitive, and open to changes of requirements and environments. The complexity makes the definition, understanding, analysis, management, and monitoring of CHWF a software engineering challenge. We propose an approach to formal modeling and analysis of CHWF. The main problems that the approach addresses are abstraction and separation of concerns through algebraic manipulation. We use the CSP process algebra for modeling and verifying the dynamic interaction behavior of processes, and discuss the relation between the dynamic model and the static model of healthcare cases and resources. We use UML models to visualize the system's behavior and structure, but definitions of the syntax and semantics of these graphical models and their relation to the CSP models are left for future work. © 2012 Springer-Verlag.
Boender J.,Middlesex University |
Fernandes S.,UNU IIST
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2014
Over the years, Free/Libre Open Source Software (FLOSS) distributions have become more and more complex and recent versions contain tens of thousands of packages. This has made it impossible to do quality control by hand. Instead, distribution editors must look to automated methods to ensure the quality of their distributions. In the present paper, we present some insights into the general structure of FLOSS distributions. We notably show that such distributions have the characteristics of a small world network: there are only a few important packages, and many less important packages. Identifying the important packages can help editors focus their efforts on parts of the distribution where errors will have important consequences. © 2014 Springer International Publishing.
Griesmayer A.,UNU IIST |
Staber S.,OneSpin Solutions |
Bloem R.,Graz University of Technology
Software Testing Verification and Reliability | Year: 2010
If a program does not fulfill its specification, a model checker can deliver a counterexample. However, although such a counterexample shows how the specification can be violated, it typically comprises large parts of the program and gives little information about which of the visited statements is responsible for the error. In this article, we show that model checkers can also be used to perform model-based diagnosis and thus fault localization. The approach leads to significantly more precise diagnoses than the state-of-the-art and typically rules out 90-99% of the code as possible fault locations. The approach is general and can be applied to any system that is amenable to model checking (with respect to language and complexity). To demonstrate the applicability and high precision of our approach, we present implementations for C programs using two different model checking tools and show experimental results from the TCAS case study and an integration with the DDVerify framework to debug Linux device drivers. Copyright © 2009 John Wiley & Sons, Ltd.
Chen Z.,National University of Defense Technology |
Liu Z.,UNU IIST |
Wang J.,National University of Defense Technology
Theoretical Computer Science | Year: 2012
Compensating CSP (cCSP) models long-running transactions. It can be used to specify service orchestrations written in programming languages like WS-BPEL. However, the original cCSP does not allow to model internal (non-deterministic) choice, synchronized parallel composition, hiding or recursion. In this paper, we introduce these operators and define for the extended language a failure-divergence (FD) semantics to allow reasoning about non-determinism, deadlock and livelock. Furthermore, we develop a refinement calculus that allows us to compare the level of non-determinism between long running transactions, and transform specifications for design and analysis. © 2012 Elsevier B.V. All rights reserved.
Faber J.,UNU IIST
2012 4th International Workshop on Software Engineering in Health Care, SEHC 2012 - Proceedings | Year: 2012
In order to precisely analyze healthcare workflows, we examine how healthcare workflows can be modeled and verified with an elementary and concise timed CSP extension. To avoid considering healthcare workflows in isolation, we investigate the usage of our CSP dialect for formally modeling workflows alongside the instruction model of the openEHR specification set, which is a general, maintainable, and interoperable approach to electronic health records. Hence, we present a CSP model for openEHR instructions, which allows timed reasoning, and also integrates a basic notion of data and undefinedness. We show that this CSP dialect is suited to verify important properties of healthcare workflows, like workflow consistency, checking against timed specifications, and resource scheduling. © 2012 IEEE.