Biblio

Found 12046 results

Filters: Keyword is Resiliency  [Clear All Filters]
2017-05-17
Schoenebeck, Grant, Snook, Aaron, Yu, Fang-Yi.  2016.  Sybil Detection Using Latent Network Structure. Proceedings of the 2016 ACM Conference on Economics and Computation. :739–756.

Sybil attacks, in which an adversary creates a large number of identities, present a formidable problem for the robustness of recommendation systems. One promising method of sybil detection is to use data from social network ties to implicitly infer trust. Previous work along this dimension typically a) assumes that it is difficult/costly for an adversary to create edges to honest nodes in the network; and b) limits the amount of damage done per such edge, using conductance-based methods. However, these methods fail to detect a simple class of sybil attacks which have been identified in online systems. Indeed, conductance-based methods seem inherently unable to do so, as they are based on the assumption that creating many edges to honest nodes is difficult, which seems to fail in real-world settings. We create a sybil defense system that accounts for the adversary's ability to launch such attacks yet provably withstands them by: Notassuminganyrestrictiononthenumberofedgesanadversarycanform,butinsteadmakingamuch weaker assumption that creating edges from sybils to most honest nodes is difficult, yet allowing that the remaining nodes can be freely connected to. Relaxing the goal from classifying all nodes as honest or sybil to the goal of classifying the "core" nodes of the network as honest; and classifying no sybil nodes as honest. Exploiting a new, for sybil detection, social network property, namely, that nodes can be embedded in low-dimensional spaces.

2017-08-02
Emmi, Michael, Enea, Constantin.  2016.  Symbolic Abstract Data Type Inference. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. :513–525.

Formal specification is a vital ingredient to scalable verification of software systems. In the case of efficient implementations of concurrent objects like atomic registers, queues, and locks, symbolic formal representations of their abstract data types (ADTs) enable efficient modular reasoning, decoupling clients from implementations. Writing adequate formal specifications, however, is a complex task requiring rare expertise. In practice, programmers write reference implementations as informal specifications. In this work we demonstrate that effective symbolic ADT representations can be automatically generated from the executions of reference implementations. Our approach exploits two key features of naturally-occurring ADTs: violations can be decomposed into a small set of representative patterns, and these patterns manifest in executions with few operations. By identifying certain algebraic properties of naturally-occurring ADTs, and exhaustively sampling executions up to a small number of operations, we generate concise symbolic ADT representations which are complete in practice, enabling the application of efficient symbolic verification algorithms without the burden of manual specification. Furthermore, the concise ADT violation patterns we generate are human-readable, and can serve as useful, formal documentation.

2017-03-27
Phull, Sona, Som, Subhranil.  2016.  Symmetric Cryptography Using Multiple Access Circular Queues (MACQ). Proceedings of the Second International Conference on Information and Communication Technology for Competitive Strategies. :107:1–107:6.

In order to provide secure data communication in present cyber space world, a stronger encryption technique becomes a necessity that can help people to protect their sensitive information from cryptanalyst. This paper proposes a novel symmetric block cipher algorithm that uses multiple access circular queues (MACQs) of variable lengths for diffusion of information to a greater extent. The keys are randomly generated and will be of variable lengths depending upon the size of each MACQ.A number of iterations of circular rotations, swapping of elements and XORing the key with queue elements are performed on each MACQ. S-box is used so that the relationship between the key and the cipher text remains indeterminate or obscure. These operations together will help in transforming the cipher into a much more complex and secure block cipher. This paper attempt to propose an encryption algorithm that is secure and fast.

2017-05-22
Pawar, Shwetambari, Jain, Nilakshi, Deshpande, Swati.  2016.  System Attribute Measures of Network Security Analyzer. Proceedings of the ACM Symposium on Women in Research 2016. :51–54.

In this paper, we have mentioned a method to find the performance of projectwhich detects various web - attacks. The project is capable to identifying and preventing attacks like SQL Injection, Cross – Site Scripting, URL rewriting, Web server 400 error code etc. The performance of system is detected using the system attributes that are mentioned in this paper. This is also used to determine efficiency of the system.

2017-11-27
Checkoway, Stephen, Maskiewicz, Jacob, Garman, Christina, Fried, Joshua, Cohney, Shaanan, Green, Matthew, Heninger, Nadia, Weinmann, Ralf-Philipp, Rescorla, Eric, Shacham, Hovav.  2016.  A Systematic Analysis of the Juniper Dual EC Incident. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :468–479.

In December 2015, Juniper Networks announced multiple security vulnerabilities stemming from unauthorized code in ScreenOS, the operating system for their NetScreen VPN routers. The more sophisticated of these vulnerabilities was a passive VPN decryption capability, enabled by a change to one of the elliptic curve points used by the Dual EC pseudorandom number generator. In this paper, we describe the results of a full independent analysis of the ScreenOS randomness and VPN key establishment protocol subsystems, which we carried out in response to this incident. While Dual EC is known to be insecure against an attacker who can choose the elliptic curve parameters, Juniper had claimed in 2013 that ScreenOS included countermeasures against this type of attack. We find that, contrary to Juniper's public statements, the ScreenOS VPN implementation has been vulnerable since 2008 to passive exploitation by an attacker who selects the Dual EC curve point. This vulnerability arises due to apparent flaws in Juniper's countermeasures as well as a cluster of changes that were all introduced concurrently with the inclusion of Dual EC in a single 2008 release. We demonstrate the vulnerability on a real NetScreen device by modifying the firmware to install our own parameters, and we show that it is possible to passively decrypt an individual VPN session in isolation without observing any other network traffic. We investigate the possibility of passively fingerprinting ScreenOS implementations in the wild. This incident is an important example of how guidelines for random number generation, engineering, and validation can fail in practice.

2017-10-13
Saeed, Ahmed, Ahmadinia, Ali, Just, Mike.  2016.  Tag-Protector: An Effective and Dynamic Detection of Out-of-bound Memory Accesses. Proceedings of the Third Workshop on Cryptography and Security in Computing Systems. :31–36.

Programming languages permitting immediate memory accesses through pointers often result in applications having memory-related errors, which may lead to unpredictable failures and security vulnerabilities. A light-weight solution is presented in this paper to tackle such illegal memory accesses dynamically in C/C++ based applications. We propose a new and effective method of instrumenting an application's source code at compile time in order to detect out-of-bound memory accesses. It is based on creating tags, to be coupled with each memory allocation and then placing additional tag checking instructions for each access made to the memory. The proposed solution is evaluated by instrumenting applications from the BugBench benchmark suite and publicly available benchmark software, Runtime Intrusion Prevention Evaluator (RIPE), detecting all the bugs successfully. The performance and memory overhead is further analysed by instrumenting and executing real world applications.

2017-05-17
Qiao, Siyi, Hu, Chengchen, Guan, Xiaohong, Zou, Jianhua.  2016.  Taming the Flow Table Overflow in OpenFlow Switch. Proceedings of the 2016 ACM SIGCOMM Conference. :591–592.

SDN has become the wide area network technology, which the academic and industry most concerned about.The limited table sizes of today’s SDN switches has turned to the most prominent short planks in the network design implementation. TCAM based flow table can provide an excellent matching performance while it really costs much. Even the flow table overflow cannot be prevented by a fixed-capacity flow table. In this paper, we design FTS(Flow Table Sharing) mechanism that can improve the performance disaster caused by overflow. We demonstrate that FTS reduces both control messages quantity and RTT time by two orders of magnitude compared to current state-of-the-art OpenFlow table-miss handler.

2017-11-20
Yoshikawa, M., Nozaki, Y..  2016.  Tamper resistance evaluation of PUF in environmental variations. 2016 IEEE Electrical Design of Advanced Packaging and Systems (EDAPS). :119–121.

The damage caused by counterfeits of semiconductors has become a serious problem. Recently, a physical unclonable function (PUF) has attracted attention as a technique to prevent counterfeiting. The present study investigates an arbiter PUF, which is a typical PUF. The vulnerability of a PUF against machine-learning attacks has been revealed. It has also been indicated that the output of a PUF is inverted from its normal output owing to the difference in environmental variations, such as the changes in power supply voltage and temperature. The resistance of a PUF against machine-learning attacks due to the difference in environmental variation has seldom been evaluated. The present study evaluated the resistance of an arbiter PUF against machine-learning attacks due to the difference in environmental variation. By performing an evaluation experiment using a simulation, the present study revealed that the resistance of an arbiter PUF against machine-learning attacks due to environmental variation was slightly improved. However, the present study also successfully predicted more than 95% of the outputs by increasing the number of learning cycles. Therefore, an arbiter PUF was revealed to be vulnerable to machine-learning attacks even after environmental variation.

Nozaki, Y., Ikezaki, Y., Yoshikawa, M..  2016.  Tamper resistance of IoT devices against electromagnnetic analysis. 2016 IEEE International Meeting for Future of Electron Devices, Kansai (IMFEDK). :1–2.

Lightweight block ciphers, which are required for IoT devices, have attracted attention. Simeck, which is one of the most popular lightweight block ciphers, can be implemented on IoT devices in the smallest area. Regarding the hardware security, the threat of electromagnetic analysis has been reported. However, electromagnetic analysis of Simeck has not been reported. Therefore, this study proposes a dedicated electromagnetic analysis for a lightweight block cipher Simeck to ensure the safety of IoT devices in the future. To our knowledge, this is the first electromagnetic analysis for Simeck. Experiments using a FPGA prove the validity of the proposed method.

2017-09-05
Luh, Robert, Schrittwieser, Sebastian, Marschalek, Stefan.  2016.  TAON: An Ontology-based Approach to Mitigating Targeted Attacks. Proceedings of the 18th International Conference on Information Integration and Web-based Applications and Services. :303–312.

Targeted attacks on IT systems are a rising threat against the confidentiality of sensitive data and the availability of systems and infrastructures. Planning for the eventuality of a data breach or sabotage attack has become an increasingly difficult task with the emergence of advanced persistent threats (APTs), a class of highly sophisticated cyber-attacks that are nigh impossible to detect using conventional signature-based systems. Understanding, interpreting, and correlating the particulars of such advanced targeted attacks is a major research challenge that needs to be tackled before behavior-based approaches can evolve from their current state to truly semantics-aware solutions. Ontologies offer a versatile foundation well suited for depicting the complex connections between such behavioral data and the diverse technical and organizational properties of an IT system. In order to facilitate the development of novel behavior-based detection systems, we present TAON, an OWL-based ontology offering a holistic view on actors, assets, and threat details, which are mapped to individual abstracted events and anomalies that can be detected by today's monitoring data providers. TOAN offers a straightforward means to plan an organization's defense against APTs and helps to understand how, why, and by whom certain resources are targeted. Populated by concrete data, the proposed ontology becomes a smart correlation framework able to combine several data sources into a semantic assessment of any targeted attack.

2017-10-04
Hayes, Jamie, Troncoso, Carmela, Danezis, George.  2016.  TASP: Towards Anonymity Sets That Persist. Proceedings of the 2016 ACM on Workshop on Privacy in the Electronic Society. :177–180.

Anonymous communication systems are vulnerable to long term passive "intersection attacks". Not all users of an anonymous communication system will be online at the same time, this leaks some information about who is talking to who. A global passive adversary observing all communications can learn the set of potential recipients of a message with more and more confidence over time. Nearly all deployed anonymous communication tools offer no protection against such attacks. In this work, we introduce TASP, a protocol used by an anonymous communication system that mitigates intersection attacks by intelligently grouping clients together into anonymity sets. We find that with a bandwidth overhead of just 8% we can dramatically extend the time necessary to perform a successful intersection attack.

2017-05-22
de Chérisey, Eloi, Guilley, Sylvain, Rioul, Olivier, Jayasinghe, Darshana.  2016.  Template Attacks with Partial Profiles and Dirichlet Priors: Application to Timing Attacks. Proceedings of the Hardware and Architectural Support for Security and Privacy 2016. :7:1–7:8.

In order to retrieve the secret key in a side-channel attack, the attacker computes distinguisher values using all the available data. A profiling stage is very useful to provide some a priori information about the leakage model. However, profiling is essentially empirical and may not be exhaustive. Therefore, during the attack, the attacker may come up on previously unseen data, which can be troublesome. A lazy workaround is to ignore all such novel observations altogether. In this paper, we show that this is not optimal and can be avoided. Our proposed techniques eventually improve the performance of classical information-theoretic distinguishers in terms of success rate.

2017-11-03
Dennis, R., Owenson, G., Aziz, B..  2016.  A Temporal Blockchain: A Formal Analysis. 2016 International Conference on Collaboration Technologies and Systems (CTS). :430–437.

This paper presents a possible solution to a fundamental limitation facing all blockchain-based systems; scalability. We propose a temporal rolling blockchain which solves the problem of its current exponential growth, instead replacing it with a constant fixed-size blockchain. We conduct a thorough analysis of related work and present a formal analysis of the new rolling blockchain, comparing the results to a traditional blockchain model to demonstrate that the deletion of data from the blockchain does not impact on the security of the proposed blockchain model before concluding our work and presenting future work to be conducted.

2017-04-24
Kuang, Liwei, Yang, Laurence T., Rho, Seungmin(Charlie), Yan, Zheng, Qiu, Kai.  2016.  A Tensor-Based Framework for Software-Defined Cloud Data Center. ACM Trans. Multimedia Comput. Commun. Appl.. 12:74:1–74:23.

Multimedia has been exponentially increasing as the biggest big data, which consist of video clips, images, and audio files. Processing and analyzing them on a cloud data center have become a preferred solution that can utilize the large pool of cloud resources to address the problems caused by the tremendous amount of unstructured multimedia data. However, there exist many challenges in processing multimedia big data on a cloud data center, such as multimedia data representation approach, an efficient networking model, and an estimation method for traffic patterns. The primary purpose of this article is to develop a novel tensor-based software-defined networking model on a cloud data center for multimedia big-data computation and communication. First, an overview of the proposed framework is provided, in which the functions of the representative modules are briefly illustrated. Then, three models,—forwarding tensor, control tensor, and transition tensor—are proposed for management of networking devices and prediction of network traffic patterns. Finally, two algorithms about single-mode and multimode tensor eigen-decomposition are developed, and the incremental method is employed for efficiently updating the generated eigen-vector and eigen-tensor. Experimental results reveal that the proposed framework is feasible and efficient to handle multimedia big data on a cloud data center.

2017-03-27
Batselier, Kim, Chen, Zhongming, Liu, Haotian, Wong, Ngai.  2016.  A Tensor-based Volterra Series Black-box Nonlinear System Identification and Simulation Framework. Proceedings of the 35th International Conference on Computer-Aided Design. :17:1–17:7.

Tensors are a multi-linear generalization of matrices to their d-way counterparts, and are receiving intense interest recently due to their natural representation of high-dimensional data and the availability of fast tensor decomposition algorithms. Given the input-output data of a nonlinear system/circuit, this paper presents a nonlinear model identification and simulation framework built on top of Volterra series and its seamless integration with tensor arithmetic. By exploiting partially-symmetric polyadic decompositions of sparse Toeplitz tensors, the proposed framework permits a pleasantly scalable way to incorporate high-order Volterra kernels. Such an approach largely eludes the curse of dimensionality and allows computationally fast modeling and simulation beyond weakly nonlinear systems. The black-box nature of the model also hides structural information of the system/circuit and encapsulates it in terms of compact tensors. Numerical examples are given to verify the efficacy, efficiency and generality of this tensor-based modeling and simulation framework.

2018-02-02
Ashok, A., Sridhar, S., McKinnon, A. D., Wang, P., Govindarasu, M..  2016.  Testbed-based performance evaluation of Attack Resilient Control for AGC. 2016 Resilience Week (RWS). :125–129.

The modern electric power grid is a complex cyber-physical system whose reliable operation is enabled by a wide-area monitoring and control infrastructure. Recent events have shown that vulnerabilities in this infrastructure may be exploited to manipulate the data being exchanged. Such a scenario could cause the associated control applications to mis-operate, potentially causing system-wide instabilities. There is a growing emphasis on looking beyond traditional cybersecurity solutions to mitigate such threats. In this paper we perform a testbed-based validation of one such solution - Attack Resilient Control (ARC) - on Iowa State University's PowerCyber testbed. ARC is a cyber-physical security solution that combines domain-specific anomaly detection and model-based mitigation to detect stealthy attacks on Automatic Generation Control (AGC). In this paper, we first describe the implementation architecture of the experiment on the testbed. Next, we demonstrate the capability of stealthy attack templates to cause forced under-frequency load shedding in a 3-area test system. We then validate the performance of ARC by measuring its ability to detect and mitigate these attacks. Our results reveal that ARC is efficient in detecting stealthy attacks and enables AGC to maintain system operating frequency close to its nominal value during an attack. Our studies also highlight the importance of testbed-based experimentation for evaluating the performance of cyber-physical security and control applications.

2017-09-26
Bertolino, Antonia, Daoudagh, Said, Lonetti, Francesca, Marchetti, Eda.  2016.  Testing Access Control Policies Against Intended Access Rights. Proceedings of the 31st Annual ACM Symposium on Applied Computing. :1641–1647.

Access Control Policies are used to specify who can access which resource under which conditions, and ensuring their correctness is vital to prevent security breaches. As access control policies can be complex and error-prone, we propose an original framework that supports the validation of the implemented policies (specified in the standard XACML notation) against the intended rights, which can be informally expressed, e.g. in tabular form. The framework relies on well-known software testing technology, such as mutation and combinatorial techniques. The paper presents the implemented environment and an application example.

2017-09-19
Xie, Tao, Enck, William.  2016.  Text Analytics for Security: Tutorial. Proceedings of the Symposium and Bootcamp on the Science of Security. :124–125.

Computing systems that make security decisions often fail to take into account human expectations. This failure occurs because human expectations are typically drawn from in textual sources (e.g., mobile application description and requirements documents) and are hard to extract and codify. Recently, researchers in security and software engineering have begun using text analytics to create initial models of human expectation. In this tutorial, we provide an introduction to popular techniques and tools of natural language processing (NLP) and text mining, and share our experiences in applying text analytics to security problems. We also highlight the current challenges of applying these techniques and tools for addressing security problems. We conclude the tutorial with discussion of future research directions.

2017-05-19
Carter, Lemuria, McBride, Maranda.  2016.  Texting While Driving Among Teens: Exploring User Perceptions to Identify Policy Recommendations. Proceedings of the 17th International Digital Government Research Conference on Digital Government Research. :375–378.

Texting while driving has emerged as a significant threat to citizen safety. In this study, we utilize general deterrence theory (GDT), protection motivation theory and personality traits to evaluate texting while driving (TWD) compliance intentions among teenage drivers. This paper presents the results of our pilot study. We administered an online survey to 105 teenage and young adult drivers. The potential implications for research and practice and policy are discussed.

2017-09-05
Huang, Haixing, Song, Jinghe, Lin, Xuelian, Ma, Shuai, Huai, Jinpeng.  2016.  TGraph: A Temporal Graph Data Management System. Proceedings of the 25th ACM International on Conference on Information and Knowledge Management. :2469–2472.

Temporal graphs are a class of graphs whose nodes and edges, together with the associated properties, continuously change over time. Recently, systems have been developed to support snapshot queries over temporal graphs. However, these systems barely support aggregate time range queries. Moreover, these systems cannot guarantee ACID transactions, an important feature for data management systems as long as concurrent processing is involved. To solve these issues, we design and develop TGraph, a temporal graph data management system, that assures the ACID transaction feature, and supports fast temporal graph queries.

2017-08-02
Chu, Pin-Yu, Tseng, Hsien-Lee.  2016.  A Theoretical Framework for Evaluating Government Open Data Platform. Proceedings of the International Conference on Electronic Governance and Open Society: Challenges in Eurasia. :135–142.

Regarding Information and Communication Technologies (ICTs) in the public sector, electronic governance is the first emerged concept which has been recognized as an important issue in government's outreach to citizens since the early 1990s. The most important development of e-governance recently is Open Government Data, which provides citizens with the opportunity to freely access government data, conduct value-added applications, provide creative public services, and participate in different kinds of democratic processes. Open Government Data is expected to enhance the quality and efficiency of government services, strengthen democratic participation, and create interests for the public and enterprises. The success of Open Government Data hinges on its accessibility, quality of data, security policy, and platform functions in general. This article presents a robust assessment framework that not only provides a valuable understanding of the development of Open Government Data but also provides an effective feedback mechanism for mid-course corrections. We further apply the framework to evaluate the Open Government Data platform of the central government, on which open data of nine major government agencies are analyzed. Our research results indicate that Financial Supervisory Commission performs better than other agencies; especially in terms of the accessibility. Financial Supervisory Commission mostly provides 3-star or above dataset formats, and the quality of its metadata is well established. However, most of the data released by government agencies are regulations, reports, operations and other administrative data, which are not immediately applicable. Overall, government agencies should enhance the amount and quality of Open Government Data positively and continuously, also strengthen the functions of discussion and linkage of platforms and the quality of datasets. Aside from consolidating collaborations and interactions to open data communities, government agencies should improve the awareness and ability of personnel to manage and apply open data. With the improvement of the level of acceptance of open data among personnel, the quantity and quality of Open Government Data would enhance as well.

2017-11-13
Urien, P..  2016.  Three Innovative Directions Based on Secure Elements for Trusted and Secured IoT Platforms. 2016 8th IFIP International Conference on New Technologies, Mobility and Security (NTMS). :1–2.

This paper presents the foundations of secured and trusted architecture for the Internet of Things platforms, based on Secure Elements (SE). Some IoT networks could be managed by service providers, dealing with smart grids or healthcare. Many platforms are using DTLS or TLS protocols. Therefore SEs running such stacks could provide strong mutual authentication and secure communications. Three future research directions are illustrated by previous experiments. TLS/DTLS SE servers for objects, CoAP DTLS clients for SIM modules, and RACS authorization servers based on SE TLS servers.

2017-05-16
Shrivastava, Anshumali, Konig, Arnd Christian, Bilenko, Mikhail.  2016.  Time Adaptive Sketches (Ada-Sketches) for Summarizing Data Streams. Proceedings of the 2016 International Conference on Management of Data. :1417–1432.

Obtaining frequency information of data streams, in limited space, is a well-recognized problem in literature. A number of recent practical applications (such as those in computational advertising) require temporally-aware solutions: obtaining historical count statistics for both time-points as well as time-ranges. In these scenarios, accuracy of estimates is typically more important for recent instances than for older ones; we call this desirable property Time Adaptiveness. With this observation, [20] introduced the Hokusai technique based on count-min sketches for estimating the frequency of any given item at any given time. The proposed approach is problematic in practice, as its memory requirements grow linearly with time, and it produces discontinuities in the estimation accuracy. In this work, we describe a new method, Time-adaptive Sketches, (Ada-sketch), that overcomes these limitations, while extending and providing a strict generalization of several popular sketching algorithms. The core idea of our method is inspired by the well-known digital Dolby noise reduction procedure that dates back to the 1960s. The theoretical analysis presented could be of independent interest in itself, as it provides clear results for the time-adaptive nature of the errors. An experimental evaluation on real streaming datasets demonstrates the superiority of the described method over Hokusai in estimating point and range queries over time. The method is simple to implement and offers a variety of design choices for future extensions. The simplicity of the procedure and the method's generalization of classic sketching techniques give hope for wide applicability of Ada-sketches in practice.

2017-05-17
Shrivastava, Aviral, Derler, Patricia, Baboud, Ya-Shian Li, Stanton, Kevin, Khayatian, Mohammad, Andrade, Hugo A., Weiss, Marc, Eidson, John, Chandhoke, Sundeep.  2016.  Time in Cyber-physical Systems. Proceedings of the Eleventh IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis. :4:1–4:10.

Many modern cyber-physical systems (CPS), especially industrial automation systems, require the actions of multiple computational systems to be performed at much higher rates and more tightly synchronized than is possible with ad hoc designs. Time is the common entity that computing and physical systems in CPS share, and correct interfacing of that is essential to flawless functionality of a CPS. Fundamental research is needed on ways to synchronize clocks of computing systems to a high degree, and on design methods that enable building blocks of CPS to perform actions at specified times. To realize the potential of CPS in the coming decades, suitable ways to specify distributed CPS applications are needed, including their timing requirements, ways to specify the timing of the CPS components (e.g. sensors, actuators, computing platform), timing analysis to determine if the application design is possible using the components, confident top-down design methodologies that can ensure that the system meets its timing requirements, and ways and methodologies to test and verify that the system meets the timing requirements. Furthermore, strategies for securing timing need to be carefully considered at every CPS design stage and not simply added on. This paper exposes these challenges of CPS development, points out limitations of previous approaches, and provides some research directions towards solving these challenges.

2017-09-26
Zhang, Zhengkui, Nielsen, Brian, Larsen, Kim G..  2016.  Time Optimal Reachability Analysis Using Swarm Verification. Proceedings of the 31st Annual ACM Symposium on Applied Computing. :1634–1640.

Time optimal reachability analysis employs model-checking to compute goal states that can be reached from an initial state with a minimal accumulated time duration. The model-checker may produce a corresponding diagnostic trace which can be interpreted as a feasible schedule for many scheduling and planning problems, response time optimization etc. We propose swarm verification to accelerate time optimal reachability using the real-time model-checker Uppaal. In swarm verification, a large number of model checker instances execute in parallel on a computer cluster using different, typically randomized search strategies. We develop four swarm algorithms and evaluate them with four models in terms scalability, and time- and memory consumption. Three of these cooperate by exchanging costs of intermediate solutions to prune the search using a branch-and-bound approach. Our results show that swarm algorithms work much faster than sequential algorithms, and especially two using combinations of random-depth-first and breadth-first show very promising performance.