Recent advances in Large Language Models demonstrate remarkable improvements in reasoning capabilities, such as DeepSeek-R1 and OpenAI-o1. However, reasoning over out-of-distribution (OOD) domains remains challenging. Existing enhancement techniques, including fine-tuning and retrieval-augmented generation, offer limited relief to this issue. While these approaches can improve factual recall and domain alignment, they do not fundamentally resolve the gap between linguistic and execution semantics. For example, autonomous agents in blockchain systems are capable of understanding commands of a decentralized governance proposal but not of carrying them out in real networks. To address this challenge, we propose a multi-agent system for OOD reasoning. The system incorporates DAOLang, a Domain-Specific Language that simplifies the specification of various governance proposals, to achieve reasoning optimization via abstract domain semantics, i.e., operational processes, conditions, and invariants that specific domain applications follow. The synthesis and improvements of DAOLang programs are based on a novel Label-Centric Retrieval algorithm and an iterative repair mechanism. A preliminary evaluation on real-world applications reflects the potential of our system in reasoning over governance proposal execution compared with existing multi-agent systems.

The processing of block lifecycles is essential to the efficiency of a blockchain, which consists of four steps: creation, execution, consensus, and validation. The permissionless blockchain systems typically had very limited transaction throughput because of the performance bottleneck of consensus protocols. With recent advances in consensus protocols, the execution and validation of transactions have become the new performance bottleneck. We propose a novel framework, called FastBlock, to speed up the execution and validation steps by introducing fine-grained concurrency. Our early design of FastBlock supported three key modules: (1) a symbolic execution-based analyzer that automatically identifies minimal atomic sections in each transaction; (2) a concurrent execution step that executes possibly conflicting transactions in parallel using hardware transactional memory; (3) a concurrent validation step that introduces a happen-before relation to deterministically re-execute transactions. The improved FastBlock presented in this article supports the nonce mechanism to schedule concurrent transactions from the same account. Moreover, we empirically study the impact of concurrency on Ethereum except for performance and shed light on potential optimizations of FastBlock. Finally, we implemented FastBlock and then evaluated the performance of FastBlock. Our result shows that the FastBlock outperforms state-of-art solutions significantly in performance: the execution step and validation step speed up to 3.0x and 2.3x on average over the original serial model, respectively, with eight concurrent threads. In addition, we evaluated the impact of the nonce mechanism, and the result shows that the performance loss caused by this mechanism is acceptable in practice.

In recent years, the confidentiality of smart contracts has become a fundamental requirement for practical applications. While many efforts have been made to develop architectural capabilities for enforcing confidential smart contracts, a few works arise to extend confidential smart contracts to Multi-Party Computation (MPC), i.e., multiple parties jointly evaluate a transaction off-chain and commit the outputs on-chain without revealing their secret inputs/outputs to each other. However, existing solutions lack public verifiability and require O(n) transactions to enable negotiation or resist adversaries, thus suffering from inefficiency and compromised security.

Collaborative development in open-source software (OSS) has long been limited by the lack of participation, i.e., A project is often maintained by an insufficient number of developers, especially for small- and medium-size projects. To establish a sustainable ecosystem for global developers and projects, we propose a decentralised and trustless open-source protocol Committable for all OSS software. The key insight behind Committable is an accountable and trusted tokenisation technology on blockchain that creates the CMT software assets for a variety of artefacts (e.g., document, code, testcase, makefile etc..) across the whole development lifecycle. A CMT token defines an abstraction of commits to OSS and systematically models the contribution from developers, therefore is far more comprehensive than a commit hash that are commonly used to identify software versions. In further, Committable introduces the Problem-Solution-Risk (PSR) framework to evaluate and reward a given set of CMT in an unbiased manner based on their contributions to a project. Owners of CMT are allowed to trade their tokens in the marketplace on blockchain established by Committable. The trading of CMT leads to transfer of token rights (e.g., sell, earn PSR rewards etc.), and more importantly, royalty to the developer for his or her original contribution. This demonstration proposal will introduce Committable on the test net of Ethereum and describe a preliminary case study with the OpenZeppelin project.

Payment channel networks (PCNs) are emerged as the most widely deployed solution to mitigate the scalability problem of permissionless cryptocurrencies, allowing vast payments to be carried out off-chain. Routing, which finds feasible paths between the senders and receivers, is critical for PCNs. However, existing solutions either fail to achieve high scalability that can maintain low storage/computation/network communication overhead, or they are susceptible to privacy disclosure. In this paper, we propose SorTEE, a service-oriented routing solution for PCNs, which adopts a set of service nodes to alleviate the per-user burden of routing and achieves more comprehensive privacy guarantees than the state-of-the-art by leveraging trusted execution environments (TEEs). SorTEE demands users communicate with the TEE by the secure channel to protect the privacy of transaction value. Then, an oblivious path mechanism is designed to construct redundant paths with the pseudo senders and receivers generated by TEEs to confuse its untrusted controller. Further, we report a novel attack that allows malicious service nodes to drop the valid paths for profit, and design a feedback mechanism to relieve it. Moreover, SorTEE hides the identities of the senders/receivers for the intermediate nodes of payment paths by introducing a novel identity information transfer scheme called encrypted identity chain. Based on security analysis and performance evaluation, our results demonstrate that SorTEE is able to achieve sufficient privacy-preserving payment and low per-user overhead.

The efficiency of block lifecycle determines the performance of blockchain, which is critically affected by the execution, mining and validation steps in blockchain lifecycle. To accelerate blockchains, many works focus on optimizing the mining step while ignoring other steps. In this paper, we propose a novel blockchain framework-FastBlock to speed up the execution and validation steps by introducing efficient concurrency. To efficiently prevent the potential concurrency violations, FastBlock utilizes symbolic execution to identify minimal atomic sections in each transaction and guarantees the atomicity of these sections in execution step via an efficient concurrency control mechanism-hardware transactional memory (HTM). To enable a deterministic validation step, FastBlock concurrently re-executes transactions based on a happen-before graph without increasing block size. Finally, we implement FastBlock and evaluate it in terms of conflicting transactions rate, number of transactions per block, and varying thread number. Our results indicate that FastBlock is efficient: the execution step and validation step speed up to 3.0x and 2.3x on average over the original serial model respectively with eight concurrent threads.

In recent years, as blockchain adoption has been expanding across a wide range of domains, e.g., digital asset, supply chain finance, etc., the confidentiality of smart contracts is now a fundamental demand for practical applications. However, while new privacy protection techniques keep coming out, how existing ones can best fit development settings is little studied. Suffering from limited architectural support in terms of programming interfaces, state-of-the-art solutions can hardly reach general developers. In this paper, we proposed the CLOAK framework for developing confidential smart contracts. The key capability of Cloak is allowing developers to implement and deploy practical solutions to multi-party transaction (MPT) problems, i.e., transact with secret inputs and states owned by different parties by simply specifying it. To this end, CLOAK introduced a domain-specific annotation language for declaring privacy specifications and further automatically generating confidential smart contracts to be deployed with trusted execution environment (TEE) on blockchain. In our evaluation on both simple and real-world applications, developers managed to deploy business services on blockchain in a concise manner by only developing CLOAK smart contracts whose size is less than 30% of the deployed ones.

Smart contracts on the Ethereum blockchain are notoriously known as vulnerable to external attacks. Many of their issues led to a considerably large financial loss as they resulted from broken payments by digital assets, e.g., cryptocurrency. Existing research focused on specific patterns to find such problems, e.g., reentrancy bug, nondeterministic recipient etc., yet may lead to false alarms or miss important issues. To mitigate these limitations, we designed the SafePay analysis framework to find unfair payments in Ethereum smart contracts. Compared to existing analyzers, SafePay can detect potential blockchain transactions with feasible exploits thus effectively avoid false reports. Specifically, the detection is driven by a systematic search for violations on fair value exchange (FVE), i.e., a new security invariant introduced in SafePay to indicate that each party “fairly” pays to others. The preliminary evaluation validated the efficacy of SafePay by reporting previously unknown issues and decreasing the number of false alarms.

While smart contracts have enabled a wide range of applications in many public blockchains, e.g., Ethereum, their security issues have been raising an increasing number of threats on the stability of blockchain ecosystem. In practice, many external attacks on smart contracts result from broken payments with digital assets, e.g., cryptocurrencies. While an increasing number of research works have been focusing on such problems, many of them adopted pattern-based heuristics (e.g., reentrancy) to find payment-related attacks thus can incur a considerably large portion of both false positives and negatives. To overcome these limitations and achieve better payment security on blockchain, we introduced a new class of payment attacks in this paper, i.e., unfair payment (UP). Compared to existing heuristics, UP semantically captures a wider range of payment attacks. Furthermore, we highlighted the general framework SAFEPAY to systematically detect UP. The key insight behind is a novel security invariant, i.e., fair value exchange (FVE), which models the fairness for blockchain payments between multiple parties. More specifically, SAFEPAY systematically explores the transaction space of a given smart contract and generates a bounded set of transaction sequences. For each of the sequence, SAFEPAY reports a UP attack once a violation on FVE is confirmed. We have further instantiated SAFEPAY for Ethereum and applied it in real-world smart contracts. In the empirical evaluation, SAFEPAY managed to identify previously unreported UP attacks and effectively avoid false alarms compared to analyzers in the literature as well.

Blockchain-based decentralized applications (DApp) have been widely adopted in different areas and trusted by more and more users due to the fact that the back end code of a DApp is publicly run on the blockchain and cannot be modified implicitly. However, there are few effective methods and tools for testing DApps and bugs can be easily introduced by inexperienced developers. The existing testing techniques either focus on testing front-end programs or back-end code but ignore the interaction between them, which makes it difficult to apply the techniques directly on DApp. In this paper, we present an automated testing technique for DApps which works in a two-phase manner. First, we employ random events to infer an abstract relation between browser-side events and blockchain-side contracts. Second, our technique generates a set of test cases under the guidance of inferred relations and orders the test cases based on a read-write graph. We also use taint analysis to track data flow of the smart contract and feed it to the generation procedure for following test cases. We have developed a tool called Sungari to implement our approach, and evaluated it on representative real-world DApps. The preliminary evaluation results demonstrated the potential of Sungari in achieving a significant optimization compared to random testing approaches.

The Ethereum ecosystem has introduced a pervasive blockchain platform with programmable transactions. Everyone is allowed to develop and deploy smart contracts. Such flexibility can lead to a large collection of similar contracts, i.e., clones, especially when Ethereum applications are highly domain-specific and may share similar functionalities within the same domain, e.g., token contracts often provide interfaces for money transfer and balance inquiry. While smart contract clones have a wide range of impact across different applications, e.g., security, they are relatively little studied. Although clone detection has been a long-standing research topic, blockchain smart contracts introduce new challenges, e.g., syntactic diversity due to trade-off between storage and execution, understanding high-level business logic etc.. In this paper, we highlighted the very first attempt to clone detection of Ethereum smart contracts. To overcome the new challenges, we introduce the concept of smart contract birthmark, i.e., a semantic-preserving and computable representation for smart contract bytecode. The birthmark captures high-level semantics by effectively sketching symbolic execution traces (e.g., data access dependencies, path conditions) and maintain syntactic regularities (e.g., type and number of instructions) as well. Then, the clone detection problem is reduced to a computation of statistical similarity between two contract birthmarks. We have implemented a clone detector called EClone and evaluated it on Ethereum. The empirical results demonstrated the potential of EClone in accurately identifying clones. We have also extended EClone for vulnerability search and managed to detect CVE-2018-10376 instances.

Low-rank metric learning aims to learn better discrimination of data subject to low-rank constraints. It keeps the intrinsic low-rank structure of datasets and reduces the time cost and memory usage in metric learning. However, it is still a challenge for current methods to handle datasets with both high dimensions and large numbers of samples. To address this issue, we present a novel fast low-rank metric learning (FLRML) method. FLRML casts the low-rank metric learning problem into an unconstrained optimization on the Stiefel manifold, which can be efficiently solved by searching along the descent curves of the manifold. FLRML significantly reduces the complexity and memory usage in optimization, which makes the method scalable to both high dimensions and large numbers of samples. Furthermore, we introduce a mini-batch version of FLRML to make the method scalable to larger datasets which are hard to be loaded and decomposed in limited memory. The outperforming experimental results show that our method is with high accuracy and much faster than the state-of-the-art methods under several benchmarks with large numbers of high-dimensional data. Code has been made available at https://github.com/highan911/FLRML.

Simulink is widely used for model-driven development (MDD) of cyber-physical systems. Typically, the Simulink-based development starts with Stateflow modeling, followed by simulation, validation, and code generation mapped to physical execution platforms. However, recent trends have raised the demands of rigorous verification on safety-critical applications to prevent intrinsic development faults and improve the system dependability, which is unfortunately challenging. Even though the constructed Stateflow model and the generated code pass the validation of Simulink Design Verifier and Simulink Polyspace, respectively, the system may still fail due to some implicit defects contained in the design model (design defect) and the generated code (implementation defects). In this article, we bridge the Stateflow-based MDD and a well-defined rigorous verification to reduce development faults. First, we develop a self-contained toolkit to translate a Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models that are missed by Simulink Design Verifier but also check more important temporal properties. Next, we customize a runtime verifier for the generated non-intrusive VHDL and C code of a Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which offers more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. In this way, safety-critical properties are both verified at the model level and at the consistent system implementation level with physical execution environment in consideration. We apply our approach to the development of a typical cyber-physical system-train communication controller based on the IEC standard 61375. Experiments show that more ambiguousness in the standard are detected and confirmed and more development faults and those corresponding errors that would lead to system failure have been removed. Furthermore, the verified implementation has been deployed on real trains.

As a result of the increasing number of concurrent programs, the researchers put forward a number of tools with different implementation strategies to detect data race. However, confirming data races from the collection of true and false positives reported by race detectors is extremely the time-consuming process during the evaluation period.

Smart contracts, as a promising and powerful application on the Ethereum blockchain, have been growing rapidly in the past few years. Since they are highly vulnerable to different forms of attacks, their security becomes a top priority. However, existing security auditing techniques are either limited in fnding vulnerabilities (rely on pre-defned bug paterns) or very expensive (rely on program analysis), thus are insufcient for Ethereum.

Race detection is increasingly popular, both in the academic research and in industrial practice. However, there is no specialized and comprehensive dataset of the data race, making it difficult to achieve the purpose of effectively evaluating race detectors or developing efficient race detection algorithms.

The Ethereum ecosystem has created a prosperity of smart contract applications in public blockchains, with transparent, traceable and programmable transactions. However, the flexibility that everybody can write and deploy smart contracts on Ethereum causes a large collection of similar contracts, i.e., clones. In practice, smart contract clones may amplify severe threats like security attacks, resource waste etc.

In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network.

Medical devices are essential for the practice of modern medicine, and the standard open-source integrated clinical environment (OpenICE) has been well designed and widely adopted to improve their interoperability. With OpenICE, it is easy to connect individual devices into the integrated clinical system to provide a coherent patient care. In this paper, we present ICERV, the first online verification approach for the OpenICE, to ensure the dependability (mainly for the safety and security) of the integrated system and the involved patient and clinician. The key idea is to customize runtime verification technique to provide a transparent verifying infrastructure to continually intercept the communication commands and messages of those devices, based on which, we can formalize the safety and security requirements as past time linear temporal logic expressions for verifier generation and online formal verification. If any requirements violate, predefined warnings or exception handling actions will be triggered timely to prevent hazards and threats. We have implemented and seamlessly integrated the approach without any changes to the source code of OpenICE nor the code of the upper-level applications or supervision, and the real device is used for evaluation to demonstrate the effectiveness.

Program obfuscation is a common practice in software development to obscure source code or binary code, in order to prevent humans from understanding the purpose or logic of software. It protects intellectual property and deters malicious attacks. While tremendous efforts have been devoted to the development of various obfuscation techniques, we have relatively little knowledge on how to most effectively use them together. The biggest challenge lies in identifying the most effective combination of obfuscation techniques. This paper presents a unified framework to optimize program obfuscation. Given an input program P and a set T of obfuscation transformations, our technique can automatically identify a sequence seq = 〈t1, t2, ..., tn〉 (∀i ∈ [1, n]. ti∈ T), such that applying ti in order on P yields the optimal obfuscation performance. We model the process of searching for seq as a mathematical optimization problem. The key technical contributions of this paper are: (1) an obscurity language model to assess obfuscation effectiveness/optimality, and (2) a guided stochastic algorithm based on Markov chain Monte Carlo methods to search for the optimal solution seq. We have realized the framework in a tool Closure* for JavaScript, and evaluated it on 25 most starred JavaScript projects on GitHub (19K lines of code). Our machinery study shows that Closure* outperforms the well-known Google Closure Compiler by defending 26% of the attacks initiated by JSNice. Our human study also reveals that Closure* is practical and can reduce the human attack success rate by 30%.

Building language models for source code enables a large set of improvements on traditional software engineering tasks. One promising application is automatic code completion. State-of-the-art techniques capture code regularities at token level with lexical information. Such language models are more suitable for predicting short token sequences, but become less effective with respect to long statement level predictions. In this paper, we have proposed PCC to optimize the token-level based language modeling. Specifically, PCC introduced an intermediate representation (IR) for source code, which puts tokens into groups using lexeme and variable relative order. In this way, PCC is able to handle long token sequences, i.e., group sequences, to suggest a complete statement with the precise synthesizer. Further more, PCC employed a fuzzy matching technique which combined genetic and longest common subsequence algorithms to make the prediction more accurate. We have implemented a code completion plugin for Eclipse and evaluated it on open-source Java projects. The results have demonstrated the potential of PCC in generating precise long statement level predictions. In 30%-60% of the cases, it can correctly suggest the complete statement with only six candidates, and 40%-90% of the cases with ten candidates.

With the rapidly growing number of online product models in construction industry, there is an urgent need for developing effective domain-specific information retrieval methods. Explicit semantic analysis (ESA) is a method that automatically extracts concept-based features from human knowledge repositories for semantic retrieval. This avoids the requirement of constructing and maintaining an explicitly formalized ontology. However, since domain-specific knowledge repositories are relatively small, the available terminologies are insufficient and concepts have coarse granularity. In this paper, we propose an enhanced ESA method for product model retrieval in construction industry. The major enhancements for the original ESA method consist of two parts. First, a novel concept expansion algorithm is proposed to solve the problem caused by insufficient terminologies. Second, a reranking algorithm is developed to solve the problem caused by coarse granularity of concepts. Experimental results show that our method significantly improves the performance of product model retrieval and outperforms the state-of-the-art methods. Our method is also applicable to product retrieval in other engineering domain if a specific knowledge repository is provided in that domain.

Synchronous embedded systems are becoming more and more complicated and are usually implemented with integrated hardware/software solutions. This implementation manner brings new challenges to the traditional model-driven design environments such as SCADE and STATEMATE, that supports pure hardware or software design. In this paper, we propose a co-design tool Tsmart-Edola to facilitate the system developers, and automatically generate the executable VHDL code and C code from the for- mal verified SyncBlock computation model. SyncBlock is a lightweight high-level system specification model with well defined syntax, simulation and formal semantics. Based on which, the graphical model editor, graphical simulator, verification translator, and code generator are implemented and seamlessly integrated into the Tsmart-Edola. For evaluation, we apply Tsmart-Edola to the design of a real-world train controller based on the international standard IEC 61375. Several critical ambiguousness or bugs in the standard are detected during formal verification of the constructed system model. Furthermore, the generated VHDL code and C code of Tsmart-Edola outperform that of the state-of-the-art tools in terms of synthesized gate array resource consumption and binary code size.

Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform.

Today's distributed systems are commonly equipped with both synchronous and asynchronous components controlled with multiple clocks. The key challenges in designing such systems are (1) how to model multi-clocked local synchronous component, local asynchronous component, and asynchronous communication among components in a single framework. (2) how to ensure the correctness of model, and keep consistency between the model and the implementation of real system. In this paper, we propose a novel computation model named GalsBlock for the design of multi-clocked embedded system with both synchronous and asynchronous components. The computation model consists of several hierarchical compound and atom blocks communicating with data port connections. Each atom block can be refined as parallel mealy automata. The synchronous component can be captured in an atom block with the corresponding local control clock while the asynchronous component in an atom block without clock, and the asynchronous communications can be captured in the data port connections among blocks. The unified operational semantics and formal semantics are defined, which can be used for simulation and verification, respectively. Then, we can generate efficient VHDL code from the validated model, which can be synthesized into the FPGA processor for execution directly. We have developed the graphical modeling, simulation, verification, and code generation toolkit to support the computation model, and applied it in the design of a sub-system used in the real train communication control.

The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit.

Architecting real-time embedded systems is of the top significance during the design phase, especially in complex applications. Due to limited time and resource, to guarantee scheduling eminence without violating application-specific constraints is a challenging problem in architecture level. In this paper, we firstly present an enhanced transformation from AADL models to Cheddar input for schedulability analysis. With subprogram and delayed connection, this transformation is feasible for complex system designs. Based on schedulability analysis, we further propose a novel architecture selection engine, which evaluates scheduling performance through selection standards and application-specific constraints via satisfaction functions. With the proposed selection engine, information from both schedulability and real-time constraints are captured to pick up an optimal architecture. We apply the proposed approach on the architecture selection of an industrial control system in railway applications. Four candidate AADL architectures are transformed and analyzed for schedulability. Then in the selection engine, candidates are ranked within two application constraints. Compared to the selection of general criteria and traditional AHP, our engine excels at better schedulability and satisfaction on real-time application-specific constraints. Moreover, with adjustment on constraints, our engine shows delicate sensitivity by generating a modified selection. We believe the proposed approach can facilitate architecture design of real-time embedded systems.

In real-time embedded applications, interrupt-driven systems are widely adopted due to strict timing requirements. However, development of interrupt-driven systems is time-consuming and error-prone. To conveniently ensure a trustworthy system design and implementation is a challenging problem, especially in complex applications. In this paper, we present a novel domain-specific language called iDola to model interrupt-driven systems declaratively and concisely. A major strength of iDola is the feasibility to capture complex interrupt handling mechanism in real-time operating systems and target platforms, such as delayed service and buffered processing. We also propose the formal operational semantics and code generation algorithm of iDola, so that iDola models can be transformed to timed automata for verification and loaded to generate platform-specific codes. We apply iDola on the modeling of an industrial interrupt-driven system, multifunction vehicle bus controller which runs in an embedded environment with eCos operating system. Based on iDola, the system is modeled with a dispatcher which embodies advanced interrupt handling in eCos, including buffered interrupt service routine and deferred service routine. Through transformation, the system design is verified and design bugs are detected. Code generation is also executed using the proposed algorithm. Generated codes display comparatively equal performance in the real system. We believe iDola can facilitate building a trustworthy interrupt-driven system.

Programmable logic controller (PLC) system is a typical kind of embedded system that is widely used in industry. The complexity of reliability analysis of safety critical PLC systems arises in handling the temporal correlations among the system components caused by the run-time execution logic of the embedded ladder program. In this paper, we propose a novel probabilistic model for the reliability analysis of PLC systems, called run-time reliability model (RRM). It is constructed based on the structure and run-time execution of the embedded ladder program, automatically. Then, we present some custom-made conditional probability distribution (CPD) tables according to the execution semantics of the RRM nodes, and insert the reliability probability of each system component referenced by the node into the corresponding CPD table. The proposed model is accurate and fast compared to previous work as described in the experiment results.