精彩導(dǎo)讀

《軟件工程》期刊始終以反映軟件工程理論、方法和技術(shù)創(chuàng)新成果，傳播軟件知識，推廣軟件應(yīng)用為己任，期望可以為促進中國軟件工程學(xué)科和軟件產(chǎn)業(yè)發(fā)展略盡綿薄之力。

★本期重點推薦論文

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

★優(yōu)秀期刊及其論文推薦

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

《IEEE軟件工程學(xué)報》關(guān)注定義明確的理論結(jié)果和經(jīng)驗研究，以及這些結(jié)果和研究對軟件構(gòu)建、分析或管理的潛在影響，范圍從制定原則的機制到將這些原則應(yīng)用于特定的環(huán)境，對軟件工程研究或?qū)嵺`者都是很有價值的。

《IEEE軟件工程學(xué)報》重點主題包括開發(fā)和維護方法及模型、評估方法、軟件項目管理、工具和環(huán)境、系統(tǒng)問題等。它涵蓋了軟件系統(tǒng)的規(guī)范、設(shè)計和實現(xiàn)的技術(shù)與原則，包括符號和過程模型，軟件測試和驗證、可靠性模型，生產(chǎn)率因素、成本模型，特定工具、集成工具環(huán)境，硬件和軟件權(quán)衡，等等。

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

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