精彩導讀

《軟件工程》期刊始終以反映軟件工程理論、方法和技術創新成果，傳播軟件知識，推廣軟件應用為己任，期望可以為促進中國軟件工程學科和軟件產業發展略盡綿薄之力。

★本期重點推薦論文

無人機本身是一個復雜的機電系統，它是機械、電子、通訊、控制、信息等技術的高度融合體，如何模擬無人機單元是這些系統開發的一個重要課題。本期發表的論文《基于半實物仿真平臺的通用無人機系統模擬器設計》提出了基于半實物仿真平臺的通用無人機模擬方案，該模擬方案比傳統數學模型或數據驅動模型更接近真實系統，更容易模擬各種故障，同時也更容易與真實系統替換，方便系統整體的開發、測試與運行。文中提出的模擬器方案是基于單元模擬的，通過對無人機系統內各個單元的數據交互和通訊協議進行抽象，以真實的接口實現單元之間的數據交互，將無人機飛行模型仿真單元嵌入系統中，實現最大程度接近真機的模擬。結果表明，該模擬方案不但可以用于總體系統的開發和調試，而且對無人機自身的研制、測試等也能起到關鍵作用。

★優秀期刊及其論文推薦

IEEE Transactions on Software Engineering，簡稱TSE，中文譯為《IEEE軟件工程學報》，網址為https：//www.computer.org/csdl/journal/ts，1975年創刊（月刊），由IEEE COMPUTER SOCIETY出版，其2019年的影響因子為6.112，排在計算機科學軟件工程領域前列，并被收入《科學引文索引擴展版》（SCIE）。

《IEEE軟件工程學報》關注定義明確的理論結果和經驗研究，以及這些結果和研究對軟件構建、分析或管理的潛在影響，范圍從制定原則的機制到將這些原則應用于特定的環境，對軟件工程研究或實踐者都是很有價值的。

《IEEE軟件工程學報》重點主題包括開發和維護方法及模型、評估方法、軟件項目管理、工具和環境、系統問題等。它涵蓋了軟件系統的規范、設計和實現的技術與原則，包括符號和過程模型，軟件測試和驗證、可靠性模型，生產率因素、成本模型，特定工具、集成工具環境，硬件和軟件權衡，等等。

2021年5月發表的“Reusing Solutions Modulo Theories”一文提出了一種復用公式解決方案的方法，它可以減少可滿足性模理論（SMT）求解器對符號程序分析可擴展性的影響。SMT求解器雖可以有效地處理相關邏輯理論中的大量表達式，但仍是符號分析（如符號執行和符號模型檢查）可擴展性的主要瓶頸。重用以前分析會話中求解公式的證明可以減少SMT求解器的調用量，從而減輕SMT求解器對符號程序分析的影響。早期，重用公式解決方案利用了結構相似公式間的等價關系和包含關系，并嚴格受限于特定的目標邏輯。作者提出了一種原始方法，該方法重用了許多公式間共享的可滿足性和不可滿足性證明，而不僅僅是等價的或含義相關的公式。這種方法可以直接跨多種邏輯進行概括。作者通過SMT求解器對五種較為流行邏輯理論的900多萬個公式進行實驗，結果證明，該方法是有效的，且具有通用性。

《軟件工程》期刊會持續為廣大讀者提供軟件工程領域方面的最新學術訊息，歡迎大家繼續支持我刊，我們共同關注軟件工程領域的發展動向，努力做好學術研究和交流工作。