Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Databases and Information Systems (234)
- Programming Languages and Compilers (184)
- Engineering (141)
- Artificial Intelligence and Robotics (134)
- Computer Engineering (125)
-
- Information Security (102)
- Graphics and Human Computer Interfaces (77)
- OS and Networks (76)
- Social and Behavioral Sciences (73)
- Numerical Analysis and Scientific Computing (56)
- Theory and Algorithms (45)
- Business (42)
- Computer and Systems Architecture (39)
- Digital Communications and Networking (38)
- Medicine and Health Sciences (31)
- Communication (29)
- Education (28)
- Health Information Technology (19)
- Systems Architecture (19)
- Sociology (18)
- Gerontology (15)
- Finance and Financial Management (14)
- Public Affairs, Public Policy and Public Administration (14)
- Higher Education (13)
- Social Media (12)
- Transportation (12)
- Technology and Innovation (11)
- Keyword
-
- Deep learning (52)
- Software engineering (45)
- Empirical study (43)
- Machine learning (33)
- Model Check (29)
-
- Software (29)
- Android (27)
- Collaboration (26)
- Deep Learning (24)
- Stack Overflow (22)
- GitHub (21)
- Fuzzing (20)
- Testing (19)
- Data mining (18)
- Programming (18)
- Computer bugs (17)
- Large language models (17)
- Security (17)
- Code search (16)
- Codes (16)
- Empirical Study (16)
- Information retrieval (16)
- Large language model (16)
- Large Language Models (15)
- Software Engineering (15)
- Software testing (15)
- Linear Temporal Logic (14)
- Vulnerability detection (14)
- Large Language Model (13)
- Semantics (13)
- Publication Year
Articles 1921 - 1950 of 2149
Full-Text Articles in Software Engineering
Auditing The Defense Against Cross Site Scripting In Web Applications, Lwin Khin Shar, Hee Beng Kuan Tan
Auditing The Defense Against Cross Site Scripting In Web Applications, Lwin Khin Shar, Hee Beng Kuan Tan
Research Collection School Of Computing and Information Systems
Majority attacks to web applications today are mainly carried out through input manipulation in order to cause unintended actions of these applications. These attacks exploit the weaknesses of web applications in preventing the manipulation of inputs. Among these attacks, cross site scripting attack -- malicious input is submitted to perform unintended actions on a HTML response page -- is a common type of attacks. This paper proposes an approach for thorough auditing of code to defend against cross site scripting attack. Based on the possible methods of implementing defenses against cross site scripting attack, the approach extracts all such defenses …
Analytics-Modulated Coding Of Surveillance Video, Lai-Tee Cheok, Nikhil Gagvani
Analytics-Modulated Coding Of Surveillance Video, Lai-Tee Cheok, Nikhil Gagvani
Research Collection School Of Computing and Information Systems
Video surveillance systems increasingly use H.264 coding to achieve 24x7 recording and streaming. However, with the proliferation of security cameras, and the need to store several months of video, bandwidth and storage costs can be significant. We propose a new compression technique to significantly improve the coding efficiency of H.264 for surveillance video. Video content is analyzed and video semantics are extracted using video analytics algorithms such as segmentation, classification and tracking. In contrast to existing approaches, our Analytics-Modulated Compression (AMC) scheme does not require coding of object shape information and produces bitstreams that are standards-compliant and not limited to …
Mining Antagonistic Communities From Social Networks, Kuan Zhang, David Lo, Ee Peng Lim
Mining Antagonistic Communities From Social Networks, Kuan Zhang, David Lo, Ee Peng Lim
Research Collection School Of Computing and Information Systems
During social interactions in a community, there are often sub-communities that behave in opposite manner. These antagonistic sub-communities could represent groups of people with opposite tastes, factions within a community distrusting one another, etc. Taking as input a set of interactions within a community, we develop a novel pattern mining approach that extracts for a set of antagonistic sub-communities. In particular, based on a set of user specified thresholds, we extract a set of pairs of sub-communities that behave in opposite ways with one another. To prevent a blow up in these set of pairs, we focus on extracting a …
A Discriminative Model Approach For Accurate Duplicate Bug Report Retrieval, Chengnian Sun, David Lo, Xiaoyin Wang, Siau-Cheng Khoo
A Discriminative Model Approach For Accurate Duplicate Bug Report Retrieval, Chengnian Sun, David Lo, Xiaoyin Wang, Siau-Cheng Khoo
Research Collection School Of Computing and Information Systems
Bug repositories are usually maintained in software projects. Testers or users submit bug reports to identify various issues with systems. Sometimes two or more bug reports correspond to the same defect. To address the problem with duplicate bug reports, a person called a triager needs to manually label these bug reports as duplicates, and link them to their "master" reports for subsequent maintenance work. However, in practice there are considerable duplicate bug reports sent daily; requesting triagers to manually label these bugs could be highly time consuming. To address this issue, recently, several techniques have be proposed using various similarity …
Awareness 2.0: Staying Aware Of Projects, Developers And Tasks Using Dashboards And Feeds, Christoph Treude, Margaret-Anne Storey
Awareness 2.0: Staying Aware Of Projects, Developers And Tasks Using Dashboards And Feeds, Christoph Treude, Margaret-Anne Storey
Research Collection School Of Computing and Information Systems
Software development teams need to maintain awareness of various different aspects ranging from overall project status and process bottlenecks to current tasks and incoming artifacts. Currently, there is a lack of theoretical foundations to guide tool selection and tool design to best support awareness tasks. In this paper, we explore how the combination of highly configurable project, team and contributor dashboards along with individual event feeds is used to accomplish extensive awareness. Our results stem from an empirical study of several large development teams, with a detailed study of a team of 150 developers and additional data from another four …
Bridging Lightweight And Heavyweight Task Organization: The Role Of Tags In Adopting New Task Categories, Christoph Treude, Margaret-Anne Storey
Bridging Lightweight And Heavyweight Task Organization: The Role Of Tags In Adopting New Task Categories, Christoph Treude, Margaret-Anne Storey
Research Collection School Of Computing and Information Systems
In collaborative software development projects, tasks are often used as a mechanism to coordinate and track shared development work. Modern development environments provide explicit support for task management where tasks are typically organized and managed through predefined categories. Although there have been many studies that analyze data available from task management systems, there has been relatively little work on the design of task management tools. In this paper we explore how tagging with freely assigned keywords provides developers with a lightweight mechanism to further categorize and annotate development tasks. We investigate how tags that are frequently used over a long …
Web2se: First Workshop On Web 2.0 For Software Engineering, Christoph Treude, Margaret-Anne Storey, Kate Ehrlich, Arie Van Deursen
Web2se: First Workshop On Web 2.0 For Software Engineering, Christoph Treude, Margaret-Anne Storey, Kate Ehrlich, Arie Van Deursen
Research Collection School Of Computing and Information Systems
Social software is built around an "architecture of participation" where user data is aggregated as a side-effect of using Web 2.0 applications. Web 2.0 implies that processes and tools are socially open, and that content can be used in several different contexts. Web 2.0 tools and technologies support interactive information sharing, data interoperability and user centered design. For instance, wikis, blogs, tags and feeds help us organize, manage and categorize content in an informal and collaborative way. One goal of this workshop is to investigate how these technologies can improve software development practices. Some of these technologies have made their …
A Comparative Exploration Of Freebsd Bug Lifetimes, Gargi Bougie, Christoph Treude, Daniel M. Germán, Margaret-Anne Storey
A Comparative Exploration Of Freebsd Bug Lifetimes, Gargi Bougie, Christoph Treude, Daniel M. Germán, Margaret-Anne Storey
Research Collection School Of Computing and Information Systems
In this paper, we explore the viability of mining the basic data provided in bug repositories to predict bug lifetimes. We follow the method of Lucas D. Panjer as described in his paper, Predicting Eclipse Bug Lifetimes. However, in place of Eclipse data, the FreeBSD bug repository is used. We compare the predictive accuracy of five different classification algorithms applied to the two data sets. In addition, we propose future work on whether there is a more informative way of classifying bugs than is considered by current bug tracking systems.
The Role Of Emergent Knowledge Structures In Collaborative Software Development, Christoph Treude
The Role Of Emergent Knowledge Structures In Collaborative Software Development, Christoph Treude
Research Collection School Of Computing and Information Systems
Many collaboration features in software development tools draw on lightweight technologies such as tagging and wikis. We propose to study the role of emergent knowledge structures created through these features. Using a mixed-methods approach, we investigate which processes emergent knowledge structures support and how tool support can leverage them.
A Scalable And Energy-Efficient Context Monitoring Framework For Mobile Personal Sensor Networks, Seungwoo Kang, Jinwon Lee, Hyukjae Jang, Youngki Lee, Souneil Park, Junehwa Song
A Scalable And Energy-Efficient Context Monitoring Framework For Mobile Personal Sensor Networks, Seungwoo Kang, Jinwon Lee, Hyukjae Jang, Youngki Lee, Souneil Park, Junehwa Song
Research Collection School Of Computing and Information Systems
The key feature of many emerging pervasive computing applications is to proactively provide services to mobile individuals. One major challenge in providing users with proactive services lies in continuously monitoring users’ context based on numerous sensors in their PAN/BAN environments. The context monitoring in such environments imposes heavy workloads on mobile devices and sensor nodes with limited computing and battery power. We present SeeMon, a scalable and energy-efficient context monitoring framework for sensor-rich, resource-limited mobile environments. Running on a personal mobile device, SeeMon effectively performs context monitoring involving numerous sensors and applications. On top of SeeMon, multiple applications on the …
The Implications Of How We Tag Software Artifacts: Exploring Different Schemata And Metadata For Tags, Christoph Treude, Margaret-Anne Storey
The Implications Of How We Tag Software Artifacts: Exploring Different Schemata And Metadata For Tags, Christoph Treude, Margaret-Anne Storey
Research Collection School Of Computing and Information Systems
Social tagging has been adopted by software developers in various contexts from source code to work items and build definitions. While the success of tagging is usually attributed to the simplicity of tags, the implementation details of tagging systems vary significantly in terms of metadata, schemata and semantics. In this position paper, we argue that academia and industry should be aware of these differences and that we should start to examine their implications.
A Social Network Based Study Of Software Team Dynamics, Subhajit Datta, Vikrant S. Kaulgoud, Vibhu Saujanya Sharma, Nishant Kumar
A Social Network Based Study Of Software Team Dynamics, Subhajit Datta, Vikrant S. Kaulgoud, Vibhu Saujanya Sharma, Nishant Kumar
Research Collection School Of Computing and Information Systems
Members of software project teams have specific roles and responsibilities which are formally defined during project inception or at the start of a life cycle activity. Often, the team structure undergoes spontaneous changes as delivery deadlines draw near and critical tasks have to be completed. Some members -- depending on their skill or seniority -- need to take on more responsibilities, while others end up being peripheral to the project's execution. We posit that this kind of ad hoc reorganization of a team's structure can be discerned from the project's bug tracker. In this paper, we extract a social network …
A Verification System For Interval-Based Specification Languages, Chunqing Chen, Jin Song Dong, Jun Sun, Andrew P. Martin
A Verification System For Interval-Based Specification Languages, Chunqing Chen, Jin Song Dong, Jun Sun, Andrew P. Martin
Research Collection School Of Computing and Information Systems
Interval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by hand becomes error-prone and difficult. In this article, we develop a verification system to facilitate the formal analysis of interval-based specification languages with machine-assisted proof support. The verification system is developed using a generic theorem prover, Prototype Verification System (PVS). Our system elaborately encodes a highly expressive set-based notation, Timed Interval Calculus (TIC), and can rigorously carry out the verification …
Policy-Driven Distributed And Collaborative Demand Response In Multi-Domain Commercial Buildings, Archan Misra, Henning Schulzrinne
Policy-Driven Distributed And Collaborative Demand Response In Multi-Domain Commercial Buildings, Archan Misra, Henning Schulzrinne
Research Collection School Of Computing and Information Systems
Enabling a sophisticated Demand Response (DR) framework, whereby individual consumers adapt their electricity consumption in response to price variations, is a major objective of the emerging Smart Grid. We first point out why the current model, of EMS-based centralized control of a static repository of high load appliances, is inappropriate for supporting DR in future commercial buildings and campuses, where the consuming appliances are controlled by multiple users. To enable DR in such multi-domain environments, we envision a more collaborative and autonomous model, where a large set of heterogeneous smart electrical devices autonomously self-organize and negotiate their collective DR. Enabling …
Playing With Recognizers: A Call For An Extensible Editor, Richard C. Davis
Playing With Recognizers: A Call For An Extensible Editor, Richard C. Davis
Research Collection School Of Computing and Information Systems
The sketch recognition interface community has not produced a -killer‖ application, because access to sketch recognition technology has been too restricted. If recognition technologies were more freely available for experimentation, powerful new applications would evolve. This paper proposes a rough architecture for an extensible graphical editor that facilitates collaboration between recognition technology developers, user interface designers, and early adopters of sketch recognition interfaces. Only by serving all three communities will we reach the critical mass necessary for killer applications to emerge.
Mashup Environments In Software Engineering, Lars Grammel, Christoph Treude, Margaret-Anne Storey
Mashup Environments In Software Engineering, Lars Grammel, Christoph Treude, Margaret-Anne Storey
Research Collection School Of Computing and Information Systems
Too often, software engineering (SE) tool research is focused on creating small, stand-alone tools that address rarely understood developer needs. We believe that research should instead provide developers with flexible environments and interoperable tools, and then study how developers appropriate and tailor these tools in practice. Although there has been some prior work on this, we feel that flexible tool environments for SE have not yet been fully explored. In particular, we propose adopting the Web 2.0 idea of mashups and mashup environments to support SE practitioners in analytic activities involving multiple information sources.
Model-Based Methods For Linking Web Service Choreography And Orchestration, Jun Sun, Yang Liu, Jin Song Dong, Geguang Pu, Tian Huat Tan
Model-Based Methods For Linking Web Service Choreography And Orchestration, Jun Sun, Yang Liu, Jin Song Dong, Geguang Pu, Tian Huat Tan
Research Collection School Of Computing and Information Systems
In recent years, many Web service composition languages have been proposed. Web service choreography describes collaboration protocols of cooperating Web service participants from a global view. Web service orchestration describes collaboration of the Web services in predefined patterns based on local decision about their interactions with one another at the message/execution level. In this work, we present model-based methods to close the gap between the two views. Building on the strength of model checking techniques, Web service choreography and orchestration are verified against temporal properties or against each other (to show that they are consistent). Specialized optimization techniques are developed …
Creating An Immersive Game World With Evolutionary Fuzzy Cognitive Maps, Yundong Cai, Ah-Hwee Tan, Zhiqi Shen, Boyang Li
Creating An Immersive Game World With Evolutionary Fuzzy Cognitive Maps, Yundong Cai, Ah-Hwee Tan, Zhiqi Shen, Boyang Li
Research Collection School Of Computing and Information Systems
An increasing number of serious games have been developed to enhance the user experiences in education and training. In order to bridge the gap of game experiences in the virtual environment and in the real life, it is crucial to generate believable characters and contexts in real-time. However, the variables to be simulated for a large-scale serious game are numerous. These variables are involved in complex causal relationships and their values change over time. In view that world modeling has not been well addressed with conventional models, this paper uses a computational model Evolutionary Fuzzy Cognitive Map (EFCM) to model …
Medially: A Provenance-Aware Remote Health Monitoring Middleware, Atanu Roy Chowdhury, Ben Falchuk, Archan Misra
Medially: A Provenance-Aware Remote Health Monitoring Middleware, Atanu Roy Chowdhury, Ben Falchuk, Archan Misra
Research Collection School Of Computing and Information Systems
This paper presents MediAlly, a middleware for supporting energy-efficient, long-term remote health monitoring. Data is collected using physiological sensors and transported back to the middleware using a smart phone. The key to MediAlly's energy efficient operations lies in the adoption of an Activity Triggered Deep Monitoring (ATDM) paradigm, where data collection episodes are triggered only when the subject is determined to possess a specified context. MediAlly supports the on-demand collection of contextual provenance using a novel low-overhead provenance collection sub-system. The behaviour of this sub-system is configured using an application-defined context composition graph. The resulting provenance stream provides valuable insight …
Workshop Report From Web2se: First Workshop On Web 2.0 For Software Engineering, Christoph Treude, Margaret-Anne Storey, Kate Ehrlich, Arie Van Deursen
Workshop Report From Web2se: First Workshop On Web 2.0 For Software Engineering, Christoph Treude, Margaret-Anne Storey, Kate Ehrlich, Arie Van Deursen
Research Collection School Of Computing and Information Systems
Web 2.0 technologies such as wikis, blogs, tags and feeds have been adopted and adapted by software engineers. With Web2SE, we provide a venue for pertinent work by highlighting current state-of-the-art research, by identifying research areas, and by discussing implications of Web 2.0 on software engineering. This paper reports on the paper presentations and the discussions among participants at Web2SE 2010 as well as on future directions of the Web2SE community.
A Review Of The Professionalization Of The Software Industry: Has It Made Software Engineering A Real Profession?, Heng Ngee Mok
A Review Of The Professionalization Of The Software Industry: Has It Made Software Engineering A Real Profession?, Heng Ngee Mok
Research Collection School Of Computing and Information Systems
Every industry strives to be called a "profession", and software engineering is no exception. This paper attempts to define "profession" from three different perspectives and provides a chronological narration of the professionalization efforts of major IT bodies such as the IEEE Computer Society, Association of Computing Machinery and British Computer Society to promote software engineering from "occupation" to "profession". The outcome of this professionalization process is then examined against the three vastly different definitions of "profession" to qualitatively gauge the success of the professionalization process.
Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong
Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Rapid development in hardware industry has brought the prevalence of multi-core systems with shared-memory, which enabled the speedup of various tasks by using parallel algorithms. The Linear Temporal Logic (LTL) model checking problem is one of the difficult problems to be parallelized or scaled up to multi-core. In this work, we propose an on-the-fly parallel model checking algorithm based on the Tarjan’s strongly connected components (SCC) detection algorithm. The approach can be applied to general LTL model checking or with different fairness assumptions. Further, it is orthogonal to state space reduction techniques like partial order reduction. We enhance our PAT …
Coherent Phrase Model For Efficient Image Near-Duplicate Retrieval, Yiqun Hu, Xiangang Cheng, Liang-Tien Chia, Xing Xie, Deepu Rajan, Ah-Hwee Tan
Coherent Phrase Model For Efficient Image Near-Duplicate Retrieval, Yiqun Hu, Xiangang Cheng, Liang-Tien Chia, Xing Xie, Deepu Rajan, Ah-Hwee Tan
Research Collection School Of Computing and Information Systems
This paper presents an efficient and effective solution for retrieving image near-duplicate (IND) from image database. We introduce the coherent phrase model which incorporates the coherency of local regions to reduce the quantization error of the bag-of-words (BoW) model. In this model, local regions are characterized by visual phrase of multiple descriptors instead of visual word of single descriptor. We propose two types of visual phrase to encode the coherency in feature and spatial domain, respectively. The proposed model reduces the number of false matches by using this coherency and generates sparse representations of images. Compared to other method, the …
Mining Hierarchical Scenario-Based Specifications, David Lo, Shahar Maoz
Mining Hierarchical Scenario-Based Specifications, David Lo, Shahar Maoz
Research Collection School Of Computing and Information Systems
Scalability over long traces, as well as comprehensibility and expressivity of results, are major challenges for dynamic analysis approaches to specification mining. In this work we present a novel use of object hierarchies over traces of inter-object method calls, as an abstraction/refinement mechanism that enables user-guided, top-down or bottom-up mining of layered scenario-based specifications, broken down by hierarchies embedded in the system under investigation. We do this using data mining methods that provide statistically significant sound and complete results modulo user-defined thresholds, in the context of Damm and Harel’s live sequence charts (LSC); a visual, modal, scenario-based, inter-object language. Thus, …
Minimum Latency Broadcasting In Multiradio, Multichannel, Multirate Wireless Meshes, Junaid Qadir, Chuntung Chou, Archan Misra, Joo Ghee Lim
Minimum Latency Broadcasting In Multiradio, Multichannel, Multirate Wireless Meshes, Junaid Qadir, Chuntung Chou, Archan Misra, Joo Ghee Lim
Research Collection School Of Computing and Information Systems
We address the problem of minimizing the worst-case broadcast delay in multi-radio multi-channel multi-rate (MR2-MC) wireless mesh networks (WMN). The problem of 'efficient' broadcast in such networks is especially challenging due to the numerous interrelated decisions that have to be made. The multi-rate transmission capability of WMN nodes, interference between wireless transmissions, and the hardness of optimal channel assignment adds complexity to our considered problem. We present four heuristic algorithms to solve the minimum latency broadcast problem for such settings and show that the 'best' performing algorithms usually adapt themselves to the available radio interfaces and channels. We also study …
User Interfaces For Visual Analysis And Monitoring In Business Intelligence, Lars Grammel, Margaret-Anne Storey, Christoph Treude
User Interfaces For Visual Analysis And Monitoring In Business Intelligence, Lars Grammel, Margaret-Anne Storey, Christoph Treude
Research Collection School Of Computing and Information Systems
Business intelligence is concerned with understanding and leveraging the vast amounts of information stored in the databases of modern enterprises. Visualization techniques have been used to make sense of this data for a long time, first in the form of simple charts, and nowadays in the form of interactive visualizations. By leveraging the strengths of the human perceptual system and incorporating user interaction, they support the flexible analysis of data as well as data monitoring by users. The recent progress in the fields of information and data visualization as well as new hardware developments and trends in business intelligence have …
Static Validation Of C Preprocessor Macros, Andreas Saebjornsen, Lingxiao Jiang, Daniel Quinlan, Zhendong Su
Static Validation Of C Preprocessor Macros, Andreas Saebjornsen, Lingxiao Jiang, Daniel Quinlan, Zhendong Su
Research Collection School Of Computing and Information Systems
The widely used C preprocessor (CPP) is generally considered a source of difficulty for understanding and maintaining C/C++ programs. The main reason for this difficulty is CPP’s purely lexical semantics, i.e., its treatment of both input and output as token streams. This can easily lead to errors that are difficult to diagnose, and it has been estimated that up to 20% of all macros are erroneous. To reduce such errors, more restrictive, replacement languages for CPP have been proposed to limit expanded macros to be valid C syntactic units. However, there is no practical tool that can effectively validate CPP …
Analysis Of Tradeoffs Between Buffer And Qos Requirements In Wireless Networks, Raphael Rom, Hwee-Pink Tan
Analysis Of Tradeoffs Between Buffer And Qos Requirements In Wireless Networks, Raphael Rom, Hwee-Pink Tan
Research Collection School Of Computing and Information Systems
In this paper, we consider the scheduling problem where data packets from K input-flows need to be delivered to K corresponding wireless receivers over a heterogeneous wireless channel. Our objective is to design a wireless scheduler that achieves good throughput and fairness performance while minimizing the buffer requirement at each wireless receiver. This is a challenging problem due to the unique characteristics of the wireless channel. We propose a novel idea of exploiting both the long-term and short-term error behavior of the wireless channel in the scheduler design. In addition to typical first-order Quality of Service (QoS) metrics such as …
Mining Quantified Temporal Rules: Formalism, Algorithms, And Evaluation, David Lo, Ganesan Ramalingam, Venkatesh-Prasad Ranganath, Kapil Vaswani
Mining Quantified Temporal Rules: Formalism, Algorithms, And Evaluation, David Lo, Ganesan Ramalingam, Venkatesh-Prasad Ranganath, Kapil Vaswani
Research Collection School Of Computing and Information Systems
Libraries usually impose constraints on how clients should use them. Often these constraints are not well-documented. In this paper, we address the problem of recovering such constraints automatically, a problem referred to as specification mining. Given some client programs that use a given library, we identify constraints on the library usage that are (almost) satisfied by the given set of clients.The class of rules we target for mining combines simple binary temporal operators with state predicates (involving equality constraints) and quantification. This is a simple yet expressive subclass of temporal properties that allows us to capture many common API usage …
Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang
Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang
Research Collection School Of Computing and Information Systems
In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are …